module Hermod.ReCon.Presburger.Internal.IR.NegNF(NegNF(..), fromQuantifierFree) where

import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import           Hermod.ReCon.Presburger.Formula (BinRel)
import           Hermod.ReCon.Presburger.Internal.IR.QuantifierFree (QuantifierFree, unfoldImplies)
import qualified Hermod.ReCon.Presburger.Internal.IR.QuantifierFree as Q

-- | Formulae in negation normal form (NNF): all negations have been pushed
--   inward past connectives via De Morgan's laws, so negation appears only at
--   the atomic level as 'IntNegBinRel' (negated comparison) or 'IntNegDiv'
--   (negated divisibility).  No @Not@ connective remains.
--   Obtained from 'Hermod.ReCon.Presburger.Internal.IR.QuantifierFree.QuantifierFree' via 'fromQuantifierFree'.
data NegNF =
     -- | φ ∨ ψ
     Or NegNF NegNF
     -- | φ ∧ ψ
   | And NegNF NegNF
     -- | T
   | Top
     -- | ⊥
   | Bottom
     -- | i = i | i < i | i ≤ i | i > i | i ≥ i
   | IntBinRel BinRel IntTerm IntTerm
     -- | ¬ (i = i) | ¬ (i < i) | ¬ (i ≤ i) | ¬ (i > i) | ¬ (i ≥ i)
   | IntNegBinRel BinRel IntTerm IntTerm
     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
   | IntDiv NatValue IntTerm
     -- | ¬ (ℕ⁺ \| i)
   | IntNegDiv NatValue IntTerm
   deriving (Int -> NegNF -> ShowS
[NegNF] -> ShowS
NegNF -> String
(Int -> NegNF -> ShowS)
-> (NegNF -> String) -> ([NegNF] -> ShowS) -> Show NegNF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NegNF -> ShowS
showsPrec :: Int -> NegNF -> ShowS
$cshow :: NegNF -> String
show :: NegNF -> String
$cshowList :: [NegNF] -> ShowS
showList :: [NegNF] -> ShowS
Show, NegNF -> NegNF -> Bool
(NegNF -> NegNF -> Bool) -> (NegNF -> NegNF -> Bool) -> Eq NegNF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NegNF -> NegNF -> Bool
== :: NegNF -> NegNF -> Bool
$c/= :: NegNF -> NegNF -> Bool
/= :: NegNF -> NegNF -> Bool
Eq, Eq NegNF
Eq NegNF =>
(NegNF -> NegNF -> Ordering)
-> (NegNF -> NegNF -> Bool)
-> (NegNF -> NegNF -> Bool)
-> (NegNF -> NegNF -> Bool)
-> (NegNF -> NegNF -> Bool)
-> (NegNF -> NegNF -> NegNF)
-> (NegNF -> NegNF -> NegNF)
-> Ord NegNF
NegNF -> NegNF -> Bool
NegNF -> NegNF -> Ordering
NegNF -> NegNF -> NegNF
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: NegNF -> NegNF -> Ordering
compare :: NegNF -> NegNF -> Ordering
$c< :: NegNF -> NegNF -> Bool
< :: NegNF -> NegNF -> Bool
$c<= :: NegNF -> NegNF -> Bool
<= :: NegNF -> NegNF -> Bool
$c> :: NegNF -> NegNF -> Bool
> :: NegNF -> NegNF -> Bool
$c>= :: NegNF -> NegNF -> Bool
>= :: NegNF -> NegNF -> Bool
$cmax :: NegNF -> NegNF -> NegNF
max :: NegNF -> NegNF -> NegNF
$cmin :: NegNF -> NegNF -> NegNF
min :: NegNF -> NegNF -> NegNF
Ord)

fromQuantifierFreeNeg :: QuantifierFree -> NegNF
fromQuantifierFreeNeg :: QuantifierFree -> NegNF
fromQuantifierFreeNeg (Q.Or QuantifierFree
a QuantifierFree
b) = NegNF -> NegNF -> NegNF
And (QuantifierFree -> NegNF
fromQuantifierFreeNeg QuantifierFree
a) (QuantifierFree -> NegNF
fromQuantifierFreeNeg QuantifierFree
b)
fromQuantifierFreeNeg (Q.And QuantifierFree
a QuantifierFree
b) = NegNF -> NegNF -> NegNF
Or (QuantifierFree -> NegNF
fromQuantifierFreeNeg QuantifierFree
a) (QuantifierFree -> NegNF
fromQuantifierFreeNeg QuantifierFree
b)
fromQuantifierFreeNeg QuantifierFree
Q.Top = NegNF
Bottom
fromQuantifierFreeNeg QuantifierFree
Q.Bottom = NegNF
Top
fromQuantifierFreeNeg (Q.IntBinRel BinRel
r IntTerm
i IntTerm
i') = BinRel -> IntTerm -> IntTerm -> NegNF
IntNegBinRel BinRel
r IntTerm
i IntTerm
i'
fromQuantifierFreeNeg (Q.IntDiv NatValue
r IntTerm
i) = NatValue -> IntTerm -> NegNF
IntNegDiv NatValue
r IntTerm
i
fromQuantifierFreeNeg (Q.Not QuantifierFree
t) = QuantifierFree -> NegNF
fromQuantifierFree QuantifierFree
t
fromQuantifierFreeNeg (Q.Implies QuantifierFree
a QuantifierFree
b) = QuantifierFree -> NegNF
fromQuantifierFreeNeg (QuantifierFree -> QuantifierFree -> QuantifierFree
unfoldImplies QuantifierFree
a QuantifierFree
b)

fromQuantifierFree :: QuantifierFree -> NegNF
fromQuantifierFree :: QuantifierFree -> NegNF
fromQuantifierFree (Q.Or QuantifierFree
a QuantifierFree
b) = NegNF -> NegNF -> NegNF
Or (QuantifierFree -> NegNF
fromQuantifierFree QuantifierFree
a) (QuantifierFree -> NegNF
fromQuantifierFree QuantifierFree
b)
fromQuantifierFree (Q.And QuantifierFree
a QuantifierFree
b) = NegNF -> NegNF -> NegNF
And (QuantifierFree -> NegNF
fromQuantifierFree QuantifierFree
a) (QuantifierFree -> NegNF
fromQuantifierFree QuantifierFree
b)
fromQuantifierFree QuantifierFree
Q.Top = NegNF
Top
fromQuantifierFree QuantifierFree
Q.Bottom = NegNF
Bottom
fromQuantifierFree (Q.IntBinRel BinRel
r IntTerm
i IntTerm
i') = BinRel -> IntTerm -> IntTerm -> NegNF
IntBinRel BinRel
r IntTerm
i IntTerm
i'
fromQuantifierFree (Q.IntDiv NatValue
r IntTerm
i) = NatValue -> IntTerm -> NegNF
IntDiv NatValue
r IntTerm
i
fromQuantifierFree (Q.Not QuantifierFree
t) = QuantifierFree -> NegNF
fromQuantifierFreeNeg QuantifierFree
t
fromQuantifierFree (Q.Implies QuantifierFree
a QuantifierFree
b) = QuantifierFree -> NegNF
fromQuantifierFree (QuantifierFree -> QuantifierFree -> QuantifierFree
unfoldImplies QuantifierFree
a QuantifierFree
b)