{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
module Copilot.Language.Spec
( Spec, Spec'
, runSpec
, SpecItem
, Observer (..)
, observer, observers
, Trigger (..)
, trigger, triggers
, arg
, Property (..)
, Prop (..)
, prop, properties
, theorem, theorems
, forall, exists
, extractProp
, Universal, Existential
) where
import Prelude hiding (not)
import Control.Monad.Writer
import Copilot.Core (Typed)
import qualified Copilot.Core as Core
import Copilot.Language.Stream
import Copilot.Theorem.Prove
type Spec = Writer [SpecItem] ()
type Spec' a = Writer [SpecItem] a
runSpec :: Spec' a -> [SpecItem]
runSpec :: forall a. Spec' a -> [SpecItem]
runSpec = forall w a. Writer w a -> w
execWriter
observers :: [SpecItem] -> [Observer]
observers :: [SpecItem] -> [Observer]
observers =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SpecItem -> [Observer] -> [Observer]
lets' []
where
lets' :: SpecItem -> [Observer] -> [Observer]
lets' SpecItem
e [Observer]
ls =
case SpecItem
e of
ObserverItem Observer
l -> Observer
l forall a. a -> [a] -> [a]
: [Observer]
ls
SpecItem
_ -> [Observer]
ls
triggers :: [SpecItem] -> [Trigger]
triggers :: [SpecItem] -> [Trigger]
triggers =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SpecItem -> [Trigger] -> [Trigger]
triggers' []
where
triggers' :: SpecItem -> [Trigger] -> [Trigger]
triggers' SpecItem
e [Trigger]
ls =
case SpecItem
e of
TriggerItem Trigger
t -> Trigger
t forall a. a -> [a] -> [a]
: [Trigger]
ls
SpecItem
_ -> [Trigger]
ls
properties :: [SpecItem] -> [Property]
properties :: [SpecItem] -> [Property]
properties =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SpecItem -> [Property] -> [Property]
properties' []
where
properties' :: SpecItem -> [Property] -> [Property]
properties' SpecItem
e [Property]
ls =
case SpecItem
e of
PropertyItem Property
p -> Property
p forall a. a -> [a] -> [a]
: [Property]
ls
SpecItem
_ -> [Property]
ls
theorems :: [SpecItem] -> [(Property, UProof)]
theorems :: [SpecItem] -> [(Property, UProof)]
theorems =
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SpecItem -> [(Property, UProof)] -> [(Property, UProof)]
theorems' []
where
theorems' :: SpecItem -> [(Property, UProof)] -> [(Property, UProof)]
theorems' SpecItem
e [(Property, UProof)]
ls =
case SpecItem
e of
TheoremItem (Property, UProof)
p -> (Property, UProof)
p forall a. a -> [a] -> [a]
: [(Property, UProof)]
ls
SpecItem
_ -> [(Property, UProof)]
ls
data SpecItem
= ObserverItem Observer
| TriggerItem Trigger
| PropertyItem Property
| TheoremItem (Property, UProof)
data Observer where
Observer :: Typed a => String -> Stream a -> Observer
observer :: Typed a
=> String
-> Stream a
-> Spec
observer :: forall a. Typed a => String -> Stream a -> Spec
observer String
name Stream a
e = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Observer -> SpecItem
ObserverItem forall a b. (a -> b) -> a -> b
$ forall a. Typed a => String -> Stream a -> Observer
Observer String
name Stream a
e]
data Trigger where
Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger
trigger :: String
-> Stream Bool
-> [Arg]
-> Spec
trigger :: String -> Stream Bool -> [Arg] -> Spec
trigger String
name Stream Bool
e [Arg]
args = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Trigger -> SpecItem
TriggerItem forall a b. (a -> b) -> a -> b
$ String -> Stream Bool -> [Arg] -> Trigger
Trigger String
name Stream Bool
e [Arg]
args]
data Property where
Property :: String -> Stream Bool -> Property
data Prop a where
Forall :: Stream Bool -> Prop Universal
Exists :: Stream Bool -> Prop Existential
forall :: Stream Bool -> Prop Universal
forall :: Stream Bool -> Prop Universal
forall = Stream Bool -> Prop Universal
Forall
exists :: Stream Bool -> Prop Existential
exists :: Stream Bool -> Prop Existential
exists = Stream Bool -> Prop Existential
Exists
extractProp :: Prop a -> Stream Bool
(Forall Stream Bool
p) = Stream Bool
p
extractProp (Exists Stream Bool
p) = Stream Bool
p
prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
prop :: forall a. String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
name Prop a
e = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Property -> SpecItem
PropertyItem forall a b. (a -> b) -> a -> b
$ String -> Stream Bool -> Property
Property String
name (forall a. Prop a -> Stream Bool
extractProp Prop a
e)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. String -> PropRef a
PropRef String
name)
theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
theorem :: forall a.
String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
theorem String
name Prop a
e (Proof UProof
p) = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [(Property, UProof) -> SpecItem
TheoremItem (String -> Stream Bool -> Property
Property String
name (forall a. Prop a -> Stream Bool
extractProp Prop a
e), UProof
p)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. String -> PropRef a
PropRef String
name)
arg :: Typed a => Stream a -> Arg
arg :: forall a. Typed a => Stream a -> Arg
arg = forall a. Typed a => Stream a -> Arg
Arg