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

{-# LANGUAGE Safe, FlexibleInstances, GADTs, MultiParamTypeClasses #-}

-- | Implement negation over quantified extensions of boolean streams.
--
-- For details, see 'Prop'.
module Copilot.Language.Operators.Propositional (not) where

import Prelude (($))

import Copilot.Language.Spec (Prop (..))
import qualified Copilot.Language.Operators.Boolean as B

import Copilot.Theorem

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

-- | A proposition that can be negated.
class Negatable a b where
  -- | Negate a proposition.
  not :: a -> b

-- | Negation of an existentially quantified proposition.
instance Negatable (Prop Existential) (Prop Universal) where
  not :: Prop Existential -> Prop Universal
not (Exists Stream Bool
p)  = Stream Bool -> Prop Universal
Forall (Stream Bool -> Prop Universal) -> Stream Bool -> Prop Universal
forall a b. (a -> b) -> a -> b
$ Stream Bool -> Stream Bool
B.not Stream Bool
p

-- | Negation of a universally quantified proposition.
instance Negatable (Prop Universal) (Prop Existential) where
  not :: Prop Universal -> Prop Existential
not (Forall Stream Bool
p)  = Stream Bool -> Prop Existential
Exists (Stream Bool -> Prop Existential)
-> Stream Bool -> Prop Existential
forall a b. (a -> b) -> a -> b
$ Stream Bool -> Stream Bool
B.not Stream Bool
p

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