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

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

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

    module Copilot.Language.Reify
      ( reify
      ) where

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

    import Copilot.Language.Analyze (analyze)
    import Copilot.Language.Error   (impossible)
    import Copilot.Language.Spec
    import Copilot.Language.Stream (Stream (..))

    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 :: forall a. Spec' a -> IO Spec
    reify 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
      refMkId         <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef Int
    0
      refVisited      <- newIORef M.empty
      refMap          <- newIORef []
      coreTriggers    <- mapM (mkTrigger  refMkId refVisited refMap) trigs
      coreObservers   <- mapM (mkObserver refMkId refVisited refMap) obsvs
      coreProperties  <- mapM (mkProperty refMkId refVisited refMap) $ props ++ (map fst thms)
      coreStreams     <- readIORef refMap

      let cspec = 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 }

      results <- sequence $ zipWith (prove cspec) (map (\(Property PropId
    n Prop a
    _,UProof
    _) -> PropId
    n) thms) $ map snd thms
      unless (and results) $ putStrLn "Warning: failed to check some proofs."

      return 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 IORef Int
    refMkId IORef (Map Int)
    refStreams IORef [Stream]
    refMap (Observer PropId
    name Stream a
    e) = do
      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
      return Core.Observer
        { Core.observerName     = name
        , Core.observerExpr     = w
        , Core.observerExprType = 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 IORef Int
    refMkId IORef (Map Int)
    refStreams IORef [Stream]
    refMap (Trigger PropId
    name Stream Bool
    guard [Arg]
    args) = do
      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
      args' <- mapM mkTriggerArg args
      return Core.Trigger
        { Core.triggerName  = name
        , Core.triggerGuard = w1
        , Core.triggerArgs  = args' }

      where

      mkTriggerArg :: Arg -> IO Core.UExpr
      mkTriggerArg :: Arg -> IO UExpr
    mkTriggerArg (Arg Stream a
    e) = do
        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
        return $ Core.UExpr typeOf 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 IORef Int
    refMkId IORef (Map Int)
    refStreams IORef [Stream]
    refMap (Property PropId
    name Prop a
    p) = do
      p' <- IORef Int -> IORef (Map Int) -> IORef [Stream] -> Prop a -> IO Prop
    forall a.
    IORef Int -> IORef (Map Int) -> IORef [Stream] -> Prop a -> IO Prop
    mkProp IORef Int
    refMkId IORef (Map Int)
    refStreams IORef [Stream]
    refMap Prop a
    p
      return Core.Property
        { Core.propertyName  = name
        , Core.propertyProp  = p' }

    -- | Transform a Copilot proposition into a Copilot Core proposition.
    mkProp :: IORef Int
           -> IORef (Map Core.Id)
           -> IORef [Core.Stream]
           -> Prop a
           -> IO Core.Prop
    mkProp :: forall a.
    IORef Int -> IORef (Map Int) -> IORef [Stream] -> Prop a -> IO Prop
    mkProp IORef Int
    refMkId IORef (Map Int)
    refStreams IORef [Stream]
    refMap Prop a
    prop =
      case Prop a
    prop of
        Forall Stream Bool
    e -> Expr Bool -> Prop
    Core.Forall (Expr Bool -> Prop) -> IO (Expr Bool) -> IO Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> 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
    e
        Exists Stream Bool
    e -> Expr Bool -> Prop
    Core.Exists (Expr Bool -> Prop) -> IO (Expr Bool) -> IO Prop
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> 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
    e

    -- | 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 :: 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 -> IO (Expr a)
    forall a. Typed a => Stream a -> IO (Expr a)
    go

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

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

        Append [a]
    _ Maybe (Stream Bool)
    _ Stream a
    _ -> do
          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
          return $ Core.Drop typeOf 0 s

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

        Drop Int
    k Stream a
    e1 -> case Stream a
    e1 of
          Append [a]
    _ Maybe (Stream Bool)
    _ Stream a
    _ -> do
              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
              return $ Core.Drop typeOf (fromIntegral k) s
          Stream a
    _ -> PropId -> PropId -> IO (Expr a)
    forall a. PropId -> PropId -> a
    impossible PropId
    "mkExpr" PropId
    "copilot-language"

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

        Const a
    x -> Expr a -> IO (Expr a)
    forall a. a -> IO 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 Stream a1
    e Stream a1 -> Stream a
    f -> do
            id <- IORef Int -> IO Int
    mkId IORef Int
    refMkId
            let cs = PropId
    "local_" PropId -> PropId -> PropId
    forall a. [a] -> [a] -> [a]
    ++ Int -> PropId
    forall a. Show a => a -> PropId
    show Int
    id
            w1 <- go e
            w2 <- go (f (Var cs))
            return $ Core.Local typeOf typeOf cs w1 w2

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

        Label PropId
    s Stream a
    e -> do
            w <- Stream a -> IO (Expr a)
    forall a. Typed a => Stream a -> IO (Expr a)
    go Stream a
    e
            return $ Core.Label typeOf s w

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

        Var PropId
    cs -> Expr a -> IO (Expr a)
    forall a. a -> IO 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 PropId
    cs Maybe [a]
    mXs -> Expr a -> IO (Expr a)
    forall a. a -> IO 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 Op1 a1 a
    op Stream a1
    e -> do
          w <- Stream a1 -> IO (Expr a1)
    forall a. Typed a => Stream a -> IO (Expr a)
    go Stream a1
    e
          return $ Core.Op1 op w

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

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

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

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

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

      mkFunArg :: Arg -> IO Core.UExpr
      mkFunArg :: Arg -> IO UExpr
    mkFunArg (Arg Stream a
    e) = do
        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
        return $ Core.UExpr typeOf w

      mkStrArg :: (Core.Name, Arg) -> IO (Core.Name, Core.UExpr)
      mkStrArg :: (PropId, Arg) -> IO (PropId, UExpr)
    mkStrArg (PropId
    name, Arg Stream a
    e) = do
        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
        return $ (name, 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 :: 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 = do
      dstn <- Stream a -> IO DynStableName
    forall a. a -> IO DynStableName
    makeDynStableName Stream a
    e0
      let Append buf _ e = e0 -- avoids warning
      mk <- haveVisited dstn
      case mk of
        Just Int
    id_ -> Int -> IO Int
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    id_
        Maybe Int
    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 DynStableName
    dstn = do
        tab <- IORef (Map Int) -> IO (Map Int)
    forall a. IORef a -> IO a
    readIORef IORef (Map Int)
    refStreams
        return (M.lookup dstn tab)

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

    -- | Create a fresh, unused 'Id'.
    mkId :: IORef Int -> IO Id
    mkId :: IORef Int -> IO Int
    mkId 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
    $ \ Int
    n -> (Int -> Int
    forall a. Enum a => a -> a
    succ Int
    n, Int
    n)