module Hermod.ReCon.Presburger.Internal.IR.CompNF(CompNF(..), fromNegNF) where
import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import qualified Hermod.ReCon.Presburger.Formula as BinRel (BinRel (..))
import           Hermod.ReCon.Presburger.Internal.IR.NegNF (NegNF)
import qualified Hermod.ReCon.Presburger.Internal.IR.NegNF as N


-- | Formulae in comparison normal form: all comparison relations have been
--   reduced to strict less-than (@<@) only.  The reductions are:
--
--   @s = t  ≡  s < t+1 ∧ t < s+1@,
--   @s ≤ t  ≡  s < t+1@,
--   @s > t  ≡  t < s@,
--   @s ≥ t  ≡  t < s+1@,
--
--   and their negations are unfolded analogously.
--   No @Implies@ or @Not@ connectives remain.
--   Obtained from 'Hermod.ReCon.Presburger.Internal.IR.NegNF.NegNF' via 'fromNegNF'.
data CompNF =
     -- | φ ∨ ψ
     Or CompNF CompNF
     -- | φ ∧ ψ
   | And CompNF CompNF
     -- | T
   | Top
     -- | ⊥
   | Bottom
     -- | i < i
   | IntLt IntTerm IntTerm
     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
   | IntDiv NatValue IntTerm
     -- | ¬ (ℕ⁺ \| i)
   | IntNegDiv NatValue IntTerm
   deriving (Int -> CompNF -> ShowS
[CompNF] -> ShowS
CompNF -> String
(Int -> CompNF -> ShowS)
-> (CompNF -> String) -> ([CompNF] -> ShowS) -> Show CompNF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CompNF -> ShowS
showsPrec :: Int -> CompNF -> ShowS
$cshow :: CompNF -> String
show :: CompNF -> String
$cshowList :: [CompNF] -> ShowS
showList :: [CompNF] -> ShowS
Show, CompNF -> CompNF -> Bool
(CompNF -> CompNF -> Bool)
-> (CompNF -> CompNF -> Bool) -> Eq CompNF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CompNF -> CompNF -> Bool
== :: CompNF -> CompNF -> Bool
$c/= :: CompNF -> CompNF -> Bool
/= :: CompNF -> CompNF -> Bool
Eq, Eq CompNF
Eq CompNF =>
(CompNF -> CompNF -> Ordering)
-> (CompNF -> CompNF -> Bool)
-> (CompNF -> CompNF -> Bool)
-> (CompNF -> CompNF -> Bool)
-> (CompNF -> CompNF -> Bool)
-> (CompNF -> CompNF -> CompNF)
-> (CompNF -> CompNF -> CompNF)
-> Ord CompNF
CompNF -> CompNF -> Bool
CompNF -> CompNF -> Ordering
CompNF -> CompNF -> CompNF
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 :: CompNF -> CompNF -> Ordering
compare :: CompNF -> CompNF -> Ordering
$c< :: CompNF -> CompNF -> Bool
< :: CompNF -> CompNF -> Bool
$c<= :: CompNF -> CompNF -> Bool
<= :: CompNF -> CompNF -> Bool
$c> :: CompNF -> CompNF -> Bool
> :: CompNF -> CompNF -> Bool
$c>= :: CompNF -> CompNF -> Bool
>= :: CompNF -> CompNF -> Bool
$cmax :: CompNF -> CompNF -> CompNF
max :: CompNF -> CompNF -> CompNF
$cmin :: CompNF -> CompNF -> CompNF
min :: CompNF -> CompNF -> CompNF
Ord)

fromNegNF :: NegNF -> CompNF
fromNegNF :: NegNF -> CompNF
fromNegNF (N.Or NegNF
a NegNF
b) = CompNF -> CompNF -> CompNF
Or (NegNF -> CompNF
fromNegNF NegNF
a) (NegNF -> CompNF
fromNegNF NegNF
b)
fromNegNF (N.And NegNF
a NegNF
b) = CompNF -> CompNF -> CompNF
And (NegNF -> CompNF
fromNegNF NegNF
a) (NegNF -> CompNF
fromNegNF NegNF
b)
fromNegNF NegNF
N.Bottom = CompNF
Bottom
fromNegNF NegNF
N.Top = CompNF
Top
-- s = t <=> s < t + 1 ∧ t < s + 1
fromNegNF (N.IntBinRel BinRel
BinRel.Eq IntTerm
s IntTerm
t) = CompNF -> CompNF -> CompNF
And (IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
t (IntValue -> IntTerm
IntConst IntValue
1))) (IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
s (IntValue -> IntTerm
IntConst IntValue
1)))
fromNegNF (N.IntBinRel BinRel
BinRel.Lt IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s IntTerm
t
-- s ≤ t <=> s < t + 1
fromNegNF (N.IntBinRel BinRel
BinRel.Lte IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
t (IntValue -> IntTerm
IntConst IntValue
1))
-- s > t <=> t < s
fromNegNF (N.IntBinRel BinRel
BinRel.Gt IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t IntTerm
s
-- s ≥ t <=> t < s + 1
fromNegNF (N.IntBinRel BinRel
BinRel.Gte IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
s (IntValue -> IntTerm
IntConst IntValue
1))
-- ¬ (s = t) <=> s < t ∨ t < s
fromNegNF (N.IntNegBinRel BinRel
BinRel.Eq IntTerm
s IntTerm
t) = CompNF -> CompNF -> CompNF
Or (IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s IntTerm
t) (IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t IntTerm
s)
-- ¬ (s < t) <=> t < s + 1
fromNegNF (N.IntNegBinRel BinRel
BinRel.Lt IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
s (IntValue -> IntTerm
IntConst IntValue
1))
-- ¬ (s ≤ t) <=> s > t <=> t < s
fromNegNF (N.IntNegBinRel BinRel
BinRel.Lte IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
t IntTerm
s
-- ¬ (s > t) <=> s ≤ t <=> s < t + 1
fromNegNF (N.IntNegBinRel BinRel
BinRel.Gt IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s (IntTerm -> IntTerm -> IntTerm
IntSum IntTerm
t (IntValue -> IntTerm
IntConst IntValue
1))
-- ¬ (s ≥ t) <=> s < t
fromNegNF (N.IntNegBinRel BinRel
BinRel.Gte IntTerm
s IntTerm
t) = IntTerm -> IntTerm -> CompNF
IntLt IntTerm
s IntTerm
t
fromNegNF (N.IntDiv NatValue
k IntTerm
t) = NatValue -> IntTerm -> CompNF
IntDiv NatValue
k IntTerm
t
fromNegNF (N.IntNegDiv NatValue
k IntTerm
t) = NatValue -> IntTerm -> CompNF
IntNegDiv NatValue
k IntTerm
t