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

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

    -- | 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