{-# LANGUAGE ExistentialQuantification #-}
{-# 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 (..), 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)
reify :: Spec' a -> IO Core.Spec
reify :: forall a. Spec' a -> IO Spec
reify Spec' a
spec = do
forall a. Spec' a -> IO ()
analyze Spec' a
spec
let trigs :: [Trigger]
trigs = [SpecItem] -> [Trigger]
triggers forall a b. (a -> b) -> a -> b
$ forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
let obsvs :: [Observer]
obsvs = [SpecItem] -> [Observer]
observers forall a b. (a -> b) -> a -> b
$ forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
let props :: [Property]
props = [SpecItem] -> [Property]
properties forall a b. (a -> b) -> a -> b
$ forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
let thms :: [(Property, UProof)]
thms = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ [SpecItem] -> [(Property, UProof)]
theorems forall a b. (a -> b) -> a -> b
$ forall a. Spec' a -> [SpecItem]
runSpec Spec' a
spec
IORef Int
refMkId <- forall a. a -> IO (IORef a)
newIORef Int
0
IORef (Map Int)
refVisited <- forall a. a -> IO (IORef a)
newIORef forall a. Map a
M.empty
IORef [Stream]
refMap <- forall a. a -> IO (IORef a)
newIORef []
[Trigger]
coreTriggers <- 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 <- 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 <- 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) forall a b. (a -> b) -> a -> b
$ [Property]
props forall a. [a] -> [a] -> [a]
++ (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Property, UProof)]
thms)
[Stream]
coreStreams <- forall a. IORef a -> IO a
readIORef IORef [Stream]
refMap
let cspec :: Spec
cspec = Core.Spec
{ specStreams :: [Stream]
Core.specStreams = 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 }
[Bool]
results <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Spec -> PropId -> UProof -> IO Bool
prove Spec
cspec) (forall a b. (a -> b) -> [a] -> [b]
map (\(Property PropId
n Stream Bool
_,UProof
_) -> PropId
n) [(Property, UProof)]
thms) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Property, UProof)]
thms
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool]
results) forall a b. (a -> b) -> a -> b
$ PropId -> IO ()
putStrLn PropId
"Warning: failed to check some proofs."
forall (m :: * -> *) a. Monad m => a -> m a
return Spec
cspec
{-# 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
Expr a
w <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return Core.Observer
{ observerName :: PropId
Core.observerName = PropId
name
, observerExpr :: Expr a
Core.observerExpr = Expr a
w
, observerExprType :: Type a
Core.observerExprType = forall a. Typed a => Type a
typeOf }
{-# 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
Expr Bool
w1 <- 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg -> IO UExpr
mkTriggerArg [Arg]
args
forall (m :: * -> *) a. Monad m => a -> m a
return 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 Stream a
e) = do
Expr a
w <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr forall a. Typed a => Type a
typeOf Expr a
w
{-# 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 Stream Bool
guard) = do
Expr Bool
w1 <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return Core.Property
{ propertyName :: PropId
Core.propertyName = PropId
name
, propertyExpr :: Expr Bool
Core.propertyExpr = Expr Bool
w1 }
{-# 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 = 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
Int
s <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> DropIdx -> Int -> Expr a
Core.Drop forall a. Typed a => Type a
typeOf DropIdx
0 Int
s
Drop Int
k Stream a
e1 -> case Stream a
e1 of
Append [a]
_ Maybe (Stream Bool)
_ Stream a
_ -> do
Int
s <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> DropIdx -> Int -> Expr a
Core.Drop forall a. Typed a => Type a
typeOf (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
k) Int
s
Stream a
_ -> forall a. PropId -> PropId -> a
impossible PropId
"mkExpr" PropId
"copilot-language"
Const a
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> a -> Expr a
Core.Const forall a. Typed a => Type a
typeOf a
x
Local Stream a
e Stream a -> Stream a
f -> do
Int
id <- IORef Int -> IO Int
mkId IORef Int
refMkId
let cs :: PropId
cs = PropId
"local_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PropId
show Int
id
Expr a
w1 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
Expr a
w2 <- forall a. Typed a => Stream a -> IO (Expr a)
go (Stream a -> Stream a
f (forall a. Typed a => PropId -> Stream a
Var PropId
cs))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a1 a.
Typeable a1 =>
Type a1 -> Type a -> PropId -> Expr a1 -> Expr a -> Expr a
Core.Local forall a. Typed a => Type a
typeOf forall a. Typed a => Type a
typeOf PropId
cs Expr a
w1 Expr a
w2
Label PropId
s Stream a
e -> do
Expr a
w <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> PropId -> Expr a -> Expr a
Core.Label forall a. Typed a => Type a
typeOf PropId
s Expr a
w
Var PropId
cs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> PropId -> Expr a
Core.Var forall a. Typed a => Type a
typeOf PropId
cs
Extern PropId
cs Maybe [a]
mXs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> PropId -> Maybe [a] -> Expr a
Core.ExternVar forall a. Typed a => Type a
typeOf PropId
cs Maybe [a]
mXs
Op1 Op1 a a
op Stream a
e -> do
Expr a
w <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a1 a. Typeable a1 => Op1 a1 a -> Expr a1 -> Expr a
Core.Op1 Op1 a a
op Expr a
w
Op2 Op2 a b a
op Stream a
e1 Stream b
e2 -> do
Expr a
w1 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e1
Expr b
w2 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream b
e2
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 Op3 a b c a
op Stream a
e1 Stream b
e2 Stream c
e3 -> do
Expr a
w1 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream a
e1
Expr b
w2 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream b
e2
Expr c
w3 <- forall a. Typed a => Stream a -> IO (Expr a)
go Stream c
e3
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 Stream a
e) = do
Expr a
w <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr 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 (PropId
name, Arg Stream a
e) = do
Expr a
w <- 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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (PropId
name, forall a. Typeable a => Type a -> Expr a -> UExpr
Core.UExpr forall a. Typed a => Type a
typeOf Expr a
w)
{-# 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
DynStableName
dstn <- forall a. a -> IO DynStableName
makeDynStableName Stream a
e0
let Append [a]
buf Maybe (Stream Bool)
_ Stream a
e = Stream a
e0
Maybe Int
mk <- DynStableName -> IO (Maybe Int)
haveVisited DynStableName
dstn
case Maybe Int
mk of
Just Int
id_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
id_
Maybe Int
Nothing -> 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
Map Int
tab <- forall a. IORef a -> IO a
readIORef IORef (Map Int)
refStreams
forall (m :: * -> *) a. Monad m => a -> m a
return (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 :: forall a. Typed a => DynStableName -> [a] -> Stream a -> IO Int
addToVisited DynStableName
dstn [a]
buf Stream a
e = do
Int
id <- IORef Int -> IO Int
mkId IORef Int
refMkId
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (Map Int)
refStreams (forall a. DynStableName -> a -> Map a -> Map a
M.insert DynStableName
dstn Int
id)
Expr a
w <- 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
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [Stream]
refMap forall a b. (a -> b) -> a -> b
$ (:)
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 = forall a. Typed a => Type a
typeOf }
forall (m :: * -> *) a. Monad m => a -> m a
return Int
id
mkId :: IORef Int -> IO Id
mkId :: IORef Int -> IO Int
mkId IORef Int
refMkId = forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef IORef Int
refMkId forall a b. (a -> b) -> a -> b
$ \ Int
n -> (forall a. Enum a => a -> a
succ Int
n, Int
n)