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

-- | Transform a Copilot Language specification into a Copilot Core
-- specification.

{-# LANGUAGE Safe #-}
{-# LANGUAGE ExistentialQuantification, Rank2Types #-}

module Copilot.Language.Reify
  ( reify
  ) where

import qualified Copilot.Core as Core
import Copilot.Core (Typed, Id, typeOf, impossible)

--import Copilot.Language.Reify.Sharing (makeSharingExplicit)
import Copilot.Language.Analyze (analyze)
import Copilot.Language.Spec
import Copilot.Language.Stream (Stream (..), Arg (..))

import Copilot.Theorem.Prove

import Prelude hiding (id)
import Data.IORef
import System.Mem.StableName.Dynamic
import System.Mem.StableName.Map (Map)
import qualified System.Mem.StableName.Map as M
import Control.Monad (liftM, unless)
--------------------------------------------------------------------------------

-- | Transform a Copilot Language specification into a Copilot Core
-- specification.
reify :: Spec' a -> IO Core.Spec
reify :: Spec' a -> IO Spec
reify spec :: Spec' a
spec = do
  Spec' a -> IO ()
forall a. Spec' a -> IO ()
analyze Spec' a
spec
  let trigs :: [Trigger]
trigs = [SpecItem] -> [Trigger]
triggers   ([SpecItem] -> [Trigger]) -> [SpecItem] -> [Trigger]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
  let obsvs :: [Observer]
obsvs = [SpecItem] -> [Observer]
observers  ([SpecItem] -> [Observer]) -> [SpecItem] -> [Observer]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
  let props :: [Property]
props = [SpecItem] -> [Property]
properties ([SpecItem] -> [Property]) -> [SpecItem] -> [Property]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
  let thms :: [(Property, UProof)]
thms  = [(Property, UProof)] -> [(Property, UProof)]
forall a. [a] -> [a]
reverse ([(Property, UProof)] -> [(Property, UProof)])
-> [(Property, UProof)] -> [(Property, UProof)]
forall a b. (a -> b) -> a -> b
$ [SpecItem] -> [(Property, UProof)]
theorems ([SpecItem] -> [(Property, UProof)])
-> [SpecItem] -> [(Property, UProof)]
forall a b. (a -> b) -> a -> b
$ Spec' a -> [SpecItem]
forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
  --let strs  = structs    $ runSpec spec
  IORef Int
refMkId         <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef 0
  IORef (Map Int)
refVisited      <- Map Int -> IO (IORef (Map Int))
forall a. a -> IO (IORef a)
newIORef Map Int
forall a. Map a
M.empty
  IORef [Stream]
refMap          <- [Stream] -> IO (IORef [Stream])
forall a. a -> IO (IORef a)
newIORef []
  [Trigger]
coreTriggers    <- (Trigger -> IO Trigger) -> [Trigger] -> IO [Trigger]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Trigger -> IO Trigger
mkTrigger  IORef Int
refMkId IORef (Map Int)
refVisited IORef [Stream]
refMap) [Trigger]
trigs
  [Observer]
coreObservers   <- (Observer -> IO Observer) -> [Observer] -> IO [Observer]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Observer -> IO Observer
mkObserver IORef Int
refMkId IORef (Map Int)
refVisited IORef [Stream]
refMap) [Observer]
obsvs
  [Property]
coreProperties  <- (Property -> IO Property) -> [Property] -> IO [Property]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Property -> IO Property
mkProperty IORef Int
refMkId IORef (Map Int)
refVisited IORef [Stream]
refMap) ([Property] -> IO [Property]) -> [Property] -> IO [Property]
forall a b. (a -> b) -> a -> b
$ [Property]
props [Property] -> [Property] -> [Property]
forall a. [a] -> [a] -> [a]
++ (((Property, UProof) -> Property)
-> [(Property, UProof)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (Property, UProof) -> Property
forall a b. (a, b) -> a
fst [(Property, UProof)]
thms)
  --coreStructs     <- mapM (mkStruct   refMkId refVisited refMap) strs
  [Stream]
coreStreams     <- IORef [Stream] -> IO [Stream]
forall a. IORef a -> IO a
readIORef IORef [Stream]
refMap

  let cspec :: Spec
cspec = Spec :: [Stream] -> [Observer] -> [Trigger] -> [Property] -> Spec
Core.Spec
        { specStreams :: [Stream]
Core.specStreams    = [Stream] -> [Stream]
forall a. [a] -> [a]
reverse [Stream]
coreStreams
        , specObservers :: [Observer]
Core.specObservers  = [Observer]
coreObservers
        , specTriggers :: [Trigger]
Core.specTriggers   = [Trigger]
coreTriggers
        , specProperties :: [Property]
Core.specProperties = [Property]
coreProperties }
        --, Core.specStructs    = coreStructs }

  [Bool]
results <- [IO Bool] -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([IO Bool] -> IO [Bool]) -> [IO Bool] -> IO [Bool]
forall a b. (a -> b) -> a -> b
$ (PropId -> UProof -> IO Bool) -> [PropId] -> [UProof] -> [IO Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Spec -> PropId -> UProof -> IO Bool
prove Spec
cspec) (((Property, UProof) -> PropId) -> [(Property, UProof)] -> [PropId]
forall a b. (a -> b) -> [a] -> [b]
map (\(Property n :: PropId
n _,_) -> PropId
n) [(Property, UProof)]
thms) ([UProof] -> [IO Bool]) -> [UProof] -> [IO Bool]
forall a b. (a -> b) -> a -> b
$ ((Property, UProof) -> UProof) -> [(Property, UProof)] -> [UProof]
forall a b. (a -> b) -> [a] -> [b]
map (Property, UProof) -> UProof
forall a b. (a, b) -> b
snd [(Property, UProof)]
thms
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
results) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ PropId -> IO ()
putStrLn "Warning: failed to check some proofs."

  Spec -> IO Spec
forall (m :: * -> *) a. Monad m => a -> m a
return Spec
cspec

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

-- | Transform a Copilot observer specification into a Copilot Core
-- observer specification.
{-# INLINE mkObserver #-}
mkObserver
  :: IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> Observer
  -> IO Core.Observer
mkObserver :: IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Observer -> IO Observer
mkObserver refMkId :: IORef Int
refMkId refStreams :: IORef (Map Int)
refStreams refMap :: IORef [Stream]
refMap (Observer name :: PropId
name e :: Stream a
e) = do
  Expr a
w <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e
  Observer -> IO Observer
forall (m :: * -> *) a. Monad m => a -> m a
return Observer :: forall a. Typeable a => PropId -> Expr a -> Type a -> Observer
Core.Observer
    { observerName :: PropId
Core.observerName     = PropId
name
    , observerExpr :: Expr a
Core.observerExpr     = Expr a
w
    , observerExprType :: Type a
Core.observerExprType = Type a
forall a. Typed a => Type a
typeOf }

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

-- | Transform a Copilot trigger specification into a Copilot Core
-- trigger specification.
{-# INLINE mkTrigger #-}
mkTrigger
  :: IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> Trigger
  -> IO Core.Trigger
mkTrigger :: IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Trigger -> IO Trigger
mkTrigger refMkId :: IORef Int
refMkId refStreams :: IORef (Map Int)
refStreams refMap :: IORef [Stream]
refMap (Trigger name :: PropId
name guard :: Stream Bool
guard args :: [Arg]
args) = do
  Expr Bool
w1 <- IORef Int
-> IORef (Map Int)
-> IORef [Stream]
-> Stream Bool
-> IO (Expr Bool)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream Bool
guard
  [UExpr]
args' <- (Arg -> IO UExpr) -> [Arg] -> IO [UExpr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg -> IO UExpr
mkTriggerArg [Arg]
args
  Trigger -> IO Trigger
forall (m :: * -> *) a. Monad m => a -> m a
return Trigger :: PropId -> Expr Bool -> [UExpr] -> Trigger
Core.Trigger
    { triggerName :: PropId
Core.triggerName  = PropId
name
    , triggerGuard :: Expr Bool
Core.triggerGuard = Expr Bool
w1
    , triggerArgs :: [UExpr]
Core.triggerArgs  = [UExpr]
args' }

  where

  mkTriggerArg :: Arg -> IO Core.UExpr
  mkTriggerArg :: Arg -> IO UExpr
mkTriggerArg (Arg e :: Stream a
e) = do
    Expr a
w <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e
    UExpr -> IO UExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (UExpr -> IO UExpr) -> UExpr -> IO UExpr
forall a b. (a -> b) -> a -> b
$ Type a -> Expr a -> UExpr
forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr Type a
forall a. Typed a => Type a
typeOf Expr a
w

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

-- | Transform a Copilot property specification into a Copilot Core
-- property specification.
{-# INLINE mkProperty #-}
mkProperty
  :: IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> Property
  -> IO Core.Property
mkProperty :: IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Property -> IO Property
mkProperty refMkId :: IORef Int
refMkId refStreams :: IORef (Map Int)
refStreams refMap :: IORef [Stream]
refMap (Property name :: PropId
name guard :: Stream Bool
guard) = do
  Expr Bool
w1 <- IORef Int
-> IORef (Map Int)
-> IORef [Stream]
-> Stream Bool
-> IO (Expr Bool)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream Bool
guard
  Property -> IO Property
forall (m :: * -> *) a. Monad m => a -> m a
return Property :: PropId -> Expr Bool -> Property
Core.Property
    { propertyName :: PropId
Core.propertyName  = PropId
name
    , propertyExpr :: Expr Bool
Core.propertyExpr  = Expr Bool
w1 }

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

--{-# INLINE mkStruct #-}
{-mkStruct
  :: IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> StructData
  -> IO Core.StructData
mkStruct refMkId refStreams refMap (StructData name fields) = do
    fields' <- mapM mkStructField fields
    return $
      Core.StructData
        { Core.structName    = name
        , Core.structFields  = fields' }

    where

    mkStructField :: String -> Arg -> IO (Core.Name, Core.UExpr)
    mkStructField cs (Arg e) = do
      w <- mkExpr refMkId refStreams refMap e
      return (cs, $ Core.UExpr typeOf w)
-}
--------------------------------------------------------------------------------


-- | Transform a Copilot stream expression into a Copilot Core expression.
{-# INLINE mkExpr #-}
mkExpr
  :: Typed a
  => IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> Stream a
  -> IO (Core.Expr a)
mkExpr :: IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr refMkId :: IORef Int
refMkId refStreams :: IORef (Map Int)
refStreams refMap :: IORef [Stream]
refMap = Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go

--  (>>= go) . makeSharingExplicit refMkId

  where
  go :: Typed a => Stream a -> IO (Core.Expr a)
  go :: Stream a -> IO (Expr a)
go e0 :: Stream a
e0 = case Stream a
e0 of

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

    Append _ _ _ -> do
      Int
s <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO Int
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO Int
mkStream IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e0
      Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> DropIdx -> Int -> Expr a
forall a. Typeable a => Type a -> DropIdx -> Int -> Expr a
Core.Drop Type a
forall a. Typed a => Type a
typeOf 0 Int
s

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

    Drop k :: Int
k e1 :: Stream a
e1 -> case Stream a
e1 of
      Append _ _ _ -> do
          Int
s <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO Int
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO Int
mkStream IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e1
          Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> DropIdx -> Int -> Expr a
forall a. Typeable a => Type a -> DropIdx -> Int -> Expr a
Core.Drop Type a
forall a. Typed a => Type a
typeOf (Int -> DropIdx
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k) Int
s
      _ -> PropId -> PropId -> IO (Expr a)
forall a. PropId -> PropId -> a
impossible "mkExpr" "copilot-language"

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

    Const x :: a
x -> Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> a -> Expr a
forall a. Typeable a => Type a -> a -> Expr a
Core.Const Type a
forall a. Typed a => Type a
typeOf a
x

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

    Local e :: Stream a
e f :: Stream a -> Stream a
f -> do
        Int
id <- IORef Int -> IO Int
mkId IORef Int
refMkId
        let cs :: PropId
cs = "local_" PropId -> PropId -> PropId
forall a. [a] -> [a] -> [a]
++ Int -> PropId
forall a. Show a => a -> PropId
show Int
id
        Expr a
w1 <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
        Expr a
w2 <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go (Stream a -> Stream a
f (PropId -> Stream a
forall a. Typed a => PropId -> Stream a
Var PropId
cs))
        Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> Type a -> PropId -> Expr a -> Expr a -> Expr a
forall a1 a.
Typeable a1 =>
Type a1 -> Type a -> PropId -> Expr a1 -> Expr a -> Expr a
Core.Local Type a
forall a. Typed a => Type a
typeOf Type a
forall a. Typed a => Type a
typeOf PropId
cs Expr a
w1 Expr a
w2

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

    Label s :: PropId
s e :: Stream a
e -> do
        Expr a
w <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
        Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> PropId -> Expr a -> Expr a
forall a. Typeable a => Type a -> PropId -> Expr a -> Expr a
Core.Label Type a
forall a. Typed a => Type a
typeOf PropId
s Expr a
w

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

    Var cs :: PropId
cs -> Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> PropId -> Expr a
forall a. Typeable a => Type a -> PropId -> Expr a
Core.Var Type a
forall a. Typed a => Type a
typeOf PropId
cs

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

    Extern cs :: PropId
cs mXs :: Maybe [a]
mXs -> Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Type a -> PropId -> Maybe [a] -> Expr a
forall a. Typeable a => Type a -> PropId -> Maybe [a] -> Expr a
Core.ExternVar Type a
forall a. Typed a => Type a
typeOf PropId
cs Maybe [a]
mXs

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

    Op1 op :: Op1 a a
op e :: Stream a
e -> do
      Expr a
w <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
      Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Op1 a a -> Expr a -> Expr a
forall a1 a. Typeable a1 => Op1 a1 a -> Expr a1 -> Expr a
Core.Op1 Op1 a a
op Expr a
w

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

    Op2 op :: Op2 a b a
op e1 :: Stream a
e1 e2 :: Stream b
e2 -> do
      Expr a
w1 <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e1
      Expr b
w2 <- Stream b -> IO (Expr b)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream b
e2
      Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Op2 a b a -> Expr a -> Expr b -> Expr a
forall a1 b a.
(Typeable a1, Typeable b) =>
Op2 a1 b a -> Expr a1 -> Expr b -> Expr a
Core.Op2 Op2 a b a
op Expr a
w1 Expr b
w2

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

    Op3 op :: Op3 a b c a
op e1 :: Stream a
e1 e2 :: Stream b
e2 e3 :: Stream c
e3 -> do
      Expr a
w1 <- Stream a -> IO (Expr a)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e1
      Expr b
w2 <- Stream b -> IO (Expr b)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream b
e2
      Expr c
w3 <- Stream c -> IO (Expr c)
forall a. Typed a => Stream a -> IO (Expr a)
go Stream c
e3
      Expr a -> IO (Expr a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr a -> IO (Expr a)) -> Expr a -> IO (Expr a)
forall a b. (a -> b) -> a -> b
$ Op3 a b c a -> Expr a -> Expr b -> Expr c -> Expr a
forall a1 b c a.
(Typeable a1, Typeable b, Typeable c) =>
Op3 a1 b c a -> Expr a1 -> Expr b -> Expr c -> Expr a
Core.Op3 Op3 a b c a
op Expr a
w1 Expr b
w2 Expr c
w3

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

  mkFunArg :: Arg -> IO Core.UExpr
  mkFunArg :: Arg -> IO UExpr
mkFunArg (Arg e :: Stream a
e) = do
    Expr a
w <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e
    UExpr -> IO UExpr
forall (m :: * -> *) a. Monad m => a -> m a
return (UExpr -> IO UExpr) -> UExpr -> IO UExpr
forall a b. (a -> b) -> a -> b
$ Type a -> Expr a -> UExpr
forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr Type a
forall a. Typed a => Type a
typeOf Expr a
w

  mkStrArg :: (Core.Name, Arg) -> IO (Core.Name, Core.UExpr)
  mkStrArg :: (PropId, Arg) -> IO (PropId, UExpr)
mkStrArg (name :: PropId
name, Arg e :: Stream a
e) = do
    Expr a
w <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e
    (PropId, UExpr) -> IO (PropId, UExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return ((PropId, UExpr) -> IO (PropId, UExpr))
-> (PropId, UExpr) -> IO (PropId, UExpr)
forall a b. (a -> b) -> a -> b
$ (PropId
name, Type a -> Expr a -> UExpr
forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr Type a
forall a. Typed a => Type a
typeOf Expr a
w)

  {-mkStructArg :: StructArg -> IO Core.SExpr
  mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do
      w <- mkExpr refMkId refStreams refMap a
      return $ Core.SExpr n $ Core.UExpr typeOf w
-}
--------------------------------------------------------------------------------

--{-# INLINE mkStruct #-}
{-mkStruct
  :: IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> StructData
  -> IO Core.StructData
mkStruct refMkId refStreams refMap (StructData name sargs) = trace (show name) $ do
  args' <- mapM mkStructArg sargs
  return $
    Core.StructData
      { Core.structName     = name
      , Core.structInst     = Core.ExternStruct typeOf "" args' Nothing }
    where
      mkStructArg (StructArg { name_ = n, arg' = Arg a }) = do
        w <- mkExpr refMkId refStreams refMap a
        return $ Core.SExpr n $ Core.UExpr typeOf w-}

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

-- | Transform a Copilot stream expression into a Copilot Core stream
-- expression.
{-# INLINE mkStream #-}
mkStream
  :: Typed a
  => IORef Int
  -> IORef (Map Core.Id)
  -> IORef [Core.Stream]
  -> Stream a
  -> IO Id
mkStream :: IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO Int
mkStream refMkId :: IORef Int
refMkId refStreams :: IORef (Map Int)
refStreams refMap :: IORef [Stream]
refMap e0 :: Stream a
e0 = do
  DynStableName
dstn <- Stream a -> IO DynStableName
forall a. a -> IO DynStableName
makeDynStableName Stream a
e0
  let Append buf _ e = Stream a
e0 -- avoids warning
  Maybe Int
mk <- DynStableName -> IO (Maybe Int)
haveVisited DynStableName
dstn
  case Maybe Int
mk of
    Just id_ :: Int
id_ -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
id_
    Nothing  -> DynStableName -> [a] -> Stream a -> IO Int
forall a. Typed a => DynStableName -> [a] -> Stream a -> IO Int
addToVisited DynStableName
dstn [a]
buf Stream a
e

  where

  {-# INLINE haveVisited #-}
  haveVisited :: DynStableName -> IO (Maybe Int)
  haveVisited :: DynStableName -> IO (Maybe Int)
haveVisited dstn :: DynStableName
dstn = do
    Map Int
tab <- IORef (Map Int) -> IO (Map Int)
forall a. IORef a -> IO a
readIORef IORef (Map Int)
refStreams
    Maybe Int -> IO (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (DynStableName -> Map Int -> Maybe Int
forall v. DynStableName -> Map v -> Maybe v
M.lookup DynStableName
dstn Map Int
tab)

  {-# INLINE addToVisited #-}
  addToVisited
    :: Typed a
    => DynStableName
    -> [a]
    -> Stream a
    -> IO Id
  addToVisited :: DynStableName -> [a] -> Stream a -> IO Int
addToVisited dstn :: DynStableName
dstn buf :: [a]
buf e :: Stream a
e = do
    Int
id <- IORef Int -> IO Int
mkId IORef Int
refMkId
    IORef (Map Int) -> (Map Int -> Map Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Map Int)
refStreams (DynStableName -> Int -> Map Int -> Map Int
forall a. DynStableName -> a -> Map a -> Map a
M.insert DynStableName
dstn Int
id)
    Expr a
w <- IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
forall a.
Typed a =>
IORef Int
-> IORef (Map Int) -> IORef [Stream] -> Stream a -> IO (Expr a)
mkExpr IORef Int
refMkId IORef (Map Int)
refStreams IORef [Stream]
refMap Stream a
e
    IORef [Stream] -> ([Stream] -> [Stream]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [Stream]
refMap (([Stream] -> [Stream]) -> IO ())
-> ([Stream] -> [Stream]) -> IO ()
forall a b. (a -> b) -> a -> b
$ (:)
      Stream :: forall a.
(Typeable a, Typed a) =>
Int -> [a] -> Expr a -> Type a -> Stream
Core.Stream
        { streamId :: Int
Core.streamId         = Int
id
        , streamBuffer :: [a]
Core.streamBuffer     = [a]
buf
        , streamExpr :: Expr a
Core.streamExpr       = Expr a
w
        , streamExprType :: Type a
Core.streamExprType   = Type a
forall a. Typed a => Type a
typeOf }
    Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
id

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

-- | Create a fresh, unused 'Id'.
mkId :: IORef Int -> IO Id
mkId :: IORef Int -> IO Int
mkId refMkId :: IORef Int
refMkId = IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef Int
refMkId ((Int -> (Int, Int)) -> IO Int) -> (Int -> (Int, Int)) -> IO Int
forall a b. (a -> b) -> a -> b
$ \ n :: Int
n -> (Int -> Int
forall a. Enum a => a -> a
succ Int
n, Int
n)