-- 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)