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

-- | Copilot specifications.

{-# LANGUAGE Safe #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}

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.Maybe (fromMaybe)

--import Copilot.Core (Typed, Struct)
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 :: Spec' a -> [SpecItem]
runSpec = Spec' a -> [SpecItem]
forall w a. Writer w a -> w
execWriter

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

observers :: [SpecItem] -> [Observer]
observers :: [SpecItem] -> [Observer]
observers =
  (SpecItem -> [Observer] -> [Observer])
-> [Observer] -> [SpecItem] -> [Observer]
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 Observer -> [Observer] -> [Observer]
forall a. a -> [a] -> [a]
: [Observer]
ls
      SpecItem
_              -> [Observer]
ls

triggers :: [SpecItem] -> [Trigger]
triggers :: [SpecItem] -> [Trigger]
triggers =
  (SpecItem -> [Trigger] -> [Trigger])
-> [Trigger] -> [SpecItem] -> [Trigger]
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 Trigger -> [Trigger] -> [Trigger]
forall a. a -> [a] -> [a]
: [Trigger]
ls
      SpecItem
_             -> [Trigger]
ls

properties :: [SpecItem] -> [Property]
properties :: [SpecItem] -> [Property]
properties =
  (SpecItem -> [Property] -> [Property])
-> [Property] -> [SpecItem] -> [Property]
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 Property -> [Property] -> [Property]
forall a. a -> [a] -> [a]
: [Property]
ls
      SpecItem
_              -> [Property]
ls

theorems :: [SpecItem] -> [(Property, UProof)]
theorems :: [SpecItem] -> [(Property, UProof)]
theorems =
  (SpecItem -> [(Property, UProof)] -> [(Property, UProof)])
-> [(Property, UProof)] -> [SpecItem] -> [(Property, UProof)]
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 (Property, UProof) -> [(Property, UProof)] -> [(Property, UProof)]
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 :: String -> Stream a -> Spec
observer String
name Stream a
e = [SpecItem] -> Spec
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Observer -> SpecItem
ObserverItem (Observer -> SpecItem) -> Observer -> SpecItem
forall a b. (a -> b) -> a -> b
$ String -> Stream a -> Observer
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 = [SpecItem] -> Spec
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Trigger -> SpecItem
TriggerItem (Trigger -> SpecItem) -> Trigger -> SpecItem
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
extractProp :: Prop a -> Stream Bool
extractProp (Forall Stream Bool
p) = Stream Bool
p
extractProp (Exists Stream Bool
p) = Stream Bool
p

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

prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
prop String
name Prop a
e = [SpecItem] -> Spec
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Property -> SpecItem
PropertyItem (Property -> SpecItem) -> Property -> SpecItem
forall a b. (a -> b) -> a -> b
$ String -> Stream Bool -> Property
Property String
name (Prop a -> Stream Bool
forall a. Prop a -> Stream Bool
extractProp Prop a
e)]
  Spec
-> Writer [SpecItem] (PropRef a) -> Writer [SpecItem] (PropRef a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropRef a -> Writer [SpecItem] (PropRef a)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> PropRef a
forall a. String -> PropRef a
PropRef String
name)

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

theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
theorem String
name Prop a
e (Proof UProof
p) = [SpecItem] -> Spec
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [(Property, UProof) -> SpecItem
TheoremItem (String -> Stream Bool -> Property
Property String
name (Prop a -> Stream Bool
forall a. Prop a -> Stream Bool
extractProp Prop a
e), UProof
p)]
  Spec
-> Writer [SpecItem] (PropRef a) -> Writer [SpecItem] (PropRef a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PropRef a -> Writer [SpecItem] (PropRef a)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> PropRef a
forall a. String -> PropRef a
PropRef String
name)

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

arg :: Typed a => Stream a -> Arg
arg :: Stream a -> Arg
arg = Stream a -> Arg
forall a. Typed a => Stream a -> Arg
Arg

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

{-
-- | Struct operator.

-- Look up the given struct x, and return field y (which should be a stream?)
(#) :: Typed a => Core.StructData -> String -> Stream a
(Core.StructData {Core.structName = x, Core.structArgs = y})#z = getField x z
  where
    getField struct_nm field_nm =
      let test = find (\(Core.StructData name _) -> name == struct_nm) structs in
      case test of
        Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"
        Just element ->
          fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structArgs))
            (error "No field by the name of \"" ++ field_nm ++ "\"") element
--(Core.StructData l m)#n = Op2 (Core.GetField Core.typeOf) (Core.StructData l m) n
-}
--------------------------------------------------------------------------------