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

-- | Let expressions.
--
-- Although Copilot is a DSL embedded in Haskell and Haskell does support let
-- expressions, we want Copilot to be able to implement explicit sharing, to
-- detect when the same stream is being used in multiple places in a
-- specification and avoid recomputing it unnecessarily.

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

module Copilot.Core.Locals
  ( Loc (..)
  , locals
  ) where

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

--------------------------------------------------------------------------------

-- | A local definition, with a given stream name and stream type.
data Loc = forall a . Loc
  { Loc -> Name
localName :: Name
  , ()
localType :: Type a }

-- | Show the underlying stream name.
instance Show Loc where
  show :: Loc -> Name
show Loc { localName :: Loc -> Name
localName = Name
name } = Name
name

--------------------------------------------------------------------------------

-- | Obtain all the local definitions in a specification.
locals :: Spec -> [Loc]
locals :: Spec -> [Loc]
locals
  Spec
    { specStreams :: Spec -> [Stream]
specStreams   = [Stream]
streams
    , specTriggers :: Spec -> [Trigger]
specTriggers  = [Trigger]
triggers
    , specObservers :: Spec -> [Observer]
specObservers = [Observer]
observers
    } = (Loc -> Loc -> Bool) -> [Loc] -> [Loc]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy Loc -> Loc -> Bool
eqLoc ([Loc] -> [Loc]) -> (DList Loc -> [Loc]) -> DList Loc -> [Loc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DList Loc -> [Loc]
forall a. DList a -> [a]
toList (DList Loc -> [Loc]) -> DList Loc -> [Loc]
forall a b. (a -> b) -> a -> b
$
          [DList Loc] -> DList Loc
forall a. [DList a] -> DList a
concat ((Stream -> DList Loc) -> [Stream] -> [DList Loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Stream -> DList Loc
locsStream   [Stream]
streams)  DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append`
          [DList Loc] -> DList Loc
forall a. [DList a] -> DList a
concat ((Trigger -> DList Loc) -> [Trigger] -> [DList Loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Trigger -> DList Loc
locsTrigger  [Trigger]
triggers) DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append`
          [DList Loc] -> DList Loc
forall a. [DList a] -> DList a
concat ((Observer -> DList Loc) -> [Observer] -> [DList Loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Observer -> DList Loc
locsObserver [Observer]
observers)

  where

  eqLoc :: Loc -> Loc -> Bool
  eqLoc :: Loc -> Loc -> Bool
eqLoc Loc { localName :: Loc -> Name
localName = Name
name1 } Loc { localName :: Loc -> Name
localName = Name
name2 } =
    Name
name1 Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
name2

--------------------------------------------------------------------------------

-- | Obtain all the local definitions in a stream.
locsStream :: Stream -> DList Loc
locsStream :: Stream -> DList Loc
locsStream Stream { streamExpr :: ()
streamExpr = Expr a
e } = Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e

--------------------------------------------------------------------------------

-- | Obtain all the local definitions in a trigger.
locsTrigger :: Trigger -> DList Loc
locsTrigger :: Trigger -> DList Loc
locsTrigger Trigger { triggerGuard :: Trigger -> Expr Bool
triggerGuard = Expr Bool
e, triggerArgs :: Trigger -> [UExpr]
triggerArgs = [UExpr]
args } =
  Expr Bool -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr Bool
e DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` [DList Loc] -> DList Loc
forall a. [DList a] -> DList a
concat ((UExpr -> DList Loc) -> [UExpr] -> [DList Loc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UExpr -> DList Loc
locsUExpr [UExpr]
args)

  where

  locsUExpr :: UExpr -> DList Loc
  locsUExpr :: UExpr -> DList Loc
locsUExpr (UExpr Type a
_ Expr a
e1) = Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e1

--------------------------------------------------------------------------------

-- | Obtain all the local definitions in an observer.
locsObserver :: Observer -> DList Loc
locsObserver :: Observer -> DList Loc
locsObserver Observer { observerExpr :: ()
observerExpr = Expr a
e } = Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e

--------------------------------------------------------------------------------

-- | Obtain all the local definitions in an expression.
locsExpr :: Expr a -> DList Loc
locsExpr :: Expr a -> DList Loc
locsExpr Expr a
e0 = case Expr a
e0 of
  Const  Type a
_ a
_             -> DList Loc
forall a. DList a
empty
  Drop   Type a
_ DropIdx
_ Int
_           -> DList Loc
forall a. DList a
empty
  Local Type a
t Type a
_ Name
name Expr a
e1 Expr a
e2   -> Loc -> DList Loc
forall a. a -> DList a
singleton (Name -> Type a -> Loc
forall a. Name -> Type a -> Loc
Loc Name
name Type a
t)
                                        DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e1
                                        DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e2
  Var Type a
_ Name
_                    -> DList Loc
forall a. DList a
empty
  ExternVar Type a
_ Name
_ Maybe [a]
_            -> DList Loc
forall a. DList a
empty
  Op1 Op1 a a
_ Expr a
e                    -> Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e
  Op2 Op2 a b a
_ Expr a
e1 Expr b
e2                -> Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e1 DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` Expr b -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr b
e2
  Op3 Op3 a b c a
_ Expr a
e1 Expr b
e2 Expr c
e3             -> Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e1 DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` Expr b -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr b
e2
                                            DList Loc -> DList Loc -> DList Loc
forall a. DList a -> DList a -> DList a
`append` Expr c -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr c
e3
  Label Type a
_ Name
_ Expr a
e                -> Expr a -> DList Loc
forall a. Expr a -> DList Loc
locsExpr Expr a
e

--------------------------------------------------------------------------------