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 Data.List (foldl')
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 = execWriter
observers :: [SpecItem] -> [Observer]
observers =
foldl' lets' []
where
lets' ls e =
case e of
ObserverItem l -> l : ls
_ -> ls
triggers :: [SpecItem] -> [Trigger]
triggers =
foldl' triggers' []
where
triggers' ls e =
case e of
TriggerItem t -> t : ls
_ -> ls
properties :: [SpecItem] -> [Property]
properties =
foldl' properties' []
where
properties' ls e =
case e of
PropertyItem p -> p : ls
_ -> ls
theorems :: [SpecItem] -> [(Property, UProof)]
theorems =
foldl' theorems' []
where
theorems' ls e =
case e of
TheoremItem p -> p : ls
_ -> 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 name e = tell [ObserverItem $ Observer name e]
data Trigger where
Trigger :: Core.Name -> Stream Bool -> [Arg] -> Trigger
trigger :: String -> Stream Bool -> [Arg] -> Spec
trigger name e args = tell [TriggerItem $ Trigger name e 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 = Forall
exists :: Stream Bool -> Prop Existential
exists = Exists
extractProp :: Prop a -> Stream Bool
extractProp (Forall p) = p
extractProp (Exists p) = p
prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
prop name e = tell [PropertyItem $ Property name (extractProp e)]
>> return (PropRef name)
theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
theorem name e (Proof p) = tell [TheoremItem (Property name (extractProp e), p)]
>> return (PropRef name)
arg :: Typed a => Stream a -> Arg
arg = Arg