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

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

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

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

class Negatable a b where
  not :: a -> b

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

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

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