module Hermod.ReCon.Presburger.Internal.IR.NormAffineDNF
  ( NormAffineDNF
  , NormAffineDNFDisjunct
  , NormAffineDNFConjunct(..)
  , IntLtForm(..)
  , IntDivForm(..)
  , fromAffineDNF
  ) where
import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import qualified Hermod.ReCon.Integer.Polynomial.Term as Term
import           Hermod.ReCon.Presburger.Internal.IR.AffineDNF (AffineDNF, AffineDNFConjunct,
                   AffineDNFDisjunct)
import qualified Hermod.ReCon.Presburger.Internal.IR.AffineDNF as Affine

import qualified Data.List as List

-- | A @<@-atom with the coefficient of @x@ normalised to 1.  Bounds take
--   the form @x < i@ ('LtL') or @i < x@ ('LtR'); constant atoms @i < j@
--   ('LtC') do not involve @x@ at all.
data IntLtForm =
    -- | x < i, where i ∈ ℤ[x̄\{x}]
    LtL IntTerm
    -- | i < x, where i ∈ ℤ⟦x̄\{x}⟧
  | LtR IntTerm
    -- i < j, where i, j ∈ ℤ⟦x̄\{x}⟧
  | LtC IntTerm IntTerm deriving (Int -> IntLtForm -> ShowS
[IntLtForm] -> ShowS
IntLtForm -> String
(Int -> IntLtForm -> ShowS)
-> (IntLtForm -> String)
-> ([IntLtForm] -> ShowS)
-> Show IntLtForm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntLtForm -> ShowS
showsPrec :: Int -> IntLtForm -> ShowS
$cshow :: IntLtForm -> String
show :: IntLtForm -> String
$cshowList :: [IntLtForm] -> ShowS
showList :: [IntLtForm] -> ShowS
Show, IntLtForm -> IntLtForm -> Bool
(IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool) -> Eq IntLtForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntLtForm -> IntLtForm -> Bool
== :: IntLtForm -> IntLtForm -> Bool
$c/= :: IntLtForm -> IntLtForm -> Bool
/= :: IntLtForm -> IntLtForm -> Bool
Eq, Eq IntLtForm
Eq IntLtForm =>
(IntLtForm -> IntLtForm -> Ordering)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> Bool)
-> (IntLtForm -> IntLtForm -> IntLtForm)
-> (IntLtForm -> IntLtForm -> IntLtForm)
-> Ord IntLtForm
IntLtForm -> IntLtForm -> Bool
IntLtForm -> IntLtForm -> Ordering
IntLtForm -> IntLtForm -> IntLtForm
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 :: IntLtForm -> IntLtForm -> Ordering
compare :: IntLtForm -> IntLtForm -> Ordering
$c< :: IntLtForm -> IntLtForm -> Bool
< :: IntLtForm -> IntLtForm -> Bool
$c<= :: IntLtForm -> IntLtForm -> Bool
<= :: IntLtForm -> IntLtForm -> Bool
$c> :: IntLtForm -> IntLtForm -> Bool
> :: IntLtForm -> IntLtForm -> Bool
$c>= :: IntLtForm -> IntLtForm -> Bool
>= :: IntLtForm -> IntLtForm -> Bool
$cmax :: IntLtForm -> IntLtForm -> IntLtForm
max :: IntLtForm -> IntLtForm -> IntLtForm
$cmin :: IntLtForm -> IntLtForm -> IntLtForm
min :: IntLtForm -> IntLtForm -> IntLtForm
Ord)

-- | A divisibility atom with the coefficient of @x@ normalised to 1.
data IntDivForm =
    -- | (h | x + i), where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
    DivL NatValue IntTerm
    -- | (h | i), where h ∈ ℕ⁺, i ∈ ℤ[x̄\{x}]
  | DivC NatValue IntTerm deriving (Int -> IntDivForm -> ShowS
[IntDivForm] -> ShowS
IntDivForm -> String
(Int -> IntDivForm -> ShowS)
-> (IntDivForm -> String)
-> ([IntDivForm] -> ShowS)
-> Show IntDivForm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntDivForm -> ShowS
showsPrec :: Int -> IntDivForm -> ShowS
$cshow :: IntDivForm -> String
show :: IntDivForm -> String
$cshowList :: [IntDivForm] -> ShowS
showList :: [IntDivForm] -> ShowS
Show, IntDivForm -> IntDivForm -> Bool
(IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool) -> Eq IntDivForm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IntDivForm -> IntDivForm -> Bool
== :: IntDivForm -> IntDivForm -> Bool
$c/= :: IntDivForm -> IntDivForm -> Bool
/= :: IntDivForm -> IntDivForm -> Bool
Eq, Eq IntDivForm
Eq IntDivForm =>
(IntDivForm -> IntDivForm -> Ordering)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> Bool)
-> (IntDivForm -> IntDivForm -> IntDivForm)
-> (IntDivForm -> IntDivForm -> IntDivForm)
-> Ord IntDivForm
IntDivForm -> IntDivForm -> Bool
IntDivForm -> IntDivForm -> Ordering
IntDivForm -> IntDivForm -> IntDivForm
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 :: IntDivForm -> IntDivForm -> Ordering
compare :: IntDivForm -> IntDivForm -> Ordering
$c< :: IntDivForm -> IntDivForm -> Bool
< :: IntDivForm -> IntDivForm -> Bool
$c<= :: IntDivForm -> IntDivForm -> Bool
<= :: IntDivForm -> IntDivForm -> Bool
$c> :: IntDivForm -> IntDivForm -> Bool
> :: IntDivForm -> IntDivForm -> Bool
$c>= :: IntDivForm -> IntDivForm -> Bool
>= :: IntDivForm -> IntDivForm -> Bool
$cmax :: IntDivForm -> IntDivForm -> IntDivForm
max :: IntDivForm -> IntDivForm -> IntDivForm
$cmin :: IntDivForm -> IntDivForm -> IntDivForm
min :: IntDivForm -> IntDivForm -> IntDivForm
Ord)

-- | A DNF conjunct in normalised affine form: the coefficient of the variable
--   @x@ being eliminated has been scaled to 1 in every atom.  This is the
--   canonical form required by Cooper's test-point enumeration step, where
--   bounds are read off directly as @x < i@ or @i < x@.
--   A 'NormAffineDNF' is a @[NormAffineDNFDisjunct]@ (disjunction) of
--   @[NormAffineDNFConjunct]@ (conjunction).
--   Produced from 'Hermod.ReCon.Presburger.Internal.IR.AffineDNF.AffineDNF' by 'fromAffineDNF'.
data NormAffineDNFConjunct =
     -- | x < i | i < x | i < j
     IntLt IntLtForm
     -- | (h | x + i) | (h | i)
   | IntDiv IntDivForm
     -- | ¬ (h | x + i) | ¬ (h | i)
   | IntNegDiv IntDivForm
   deriving (Int -> NormAffineDNFConjunct -> ShowS
[NormAffineDNFConjunct] -> ShowS
NormAffineDNFConjunct -> String
(Int -> NormAffineDNFConjunct -> ShowS)
-> (NormAffineDNFConjunct -> String)
-> ([NormAffineDNFConjunct] -> ShowS)
-> Show NormAffineDNFConjunct
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NormAffineDNFConjunct -> ShowS
showsPrec :: Int -> NormAffineDNFConjunct -> ShowS
$cshow :: NormAffineDNFConjunct -> String
show :: NormAffineDNFConjunct -> String
$cshowList :: [NormAffineDNFConjunct] -> ShowS
showList :: [NormAffineDNFConjunct] -> ShowS
Show, NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
(NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> (NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> Eq NormAffineDNFConjunct
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
== :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
$c/= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
/= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
Eq, Eq NormAffineDNFConjunct
Eq NormAffineDNFConjunct =>
(NormAffineDNFConjunct -> NormAffineDNFConjunct -> Ordering)
-> (NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> (NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> (NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> (NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool)
-> (NormAffineDNFConjunct
    -> NormAffineDNFConjunct -> NormAffineDNFConjunct)
-> (NormAffineDNFConjunct
    -> NormAffineDNFConjunct -> NormAffineDNFConjunct)
-> Ord NormAffineDNFConjunct
NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
NormAffineDNFConjunct -> NormAffineDNFConjunct -> Ordering
NormAffineDNFConjunct
-> NormAffineDNFConjunct -> NormAffineDNFConjunct
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 :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Ordering
compare :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Ordering
$c< :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
< :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
$c<= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
<= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
$c> :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
> :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
$c>= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
>= :: NormAffineDNFConjunct -> NormAffineDNFConjunct -> Bool
$cmax :: NormAffineDNFConjunct
-> NormAffineDNFConjunct -> NormAffineDNFConjunct
max :: NormAffineDNFConjunct
-> NormAffineDNFConjunct -> NormAffineDNFConjunct
$cmin :: NormAffineDNFConjunct
-> NormAffineDNFConjunct -> NormAffineDNFConjunct
min :: NormAffineDNFConjunct
-> NormAffineDNFConjunct -> NormAffineDNFConjunct
Ord)

type NormAffineDNFDisjunct = [NormAffineDNFConjunct]

type NormAffineDNF = [NormAffineDNFDisjunct]

detIntLtForm :: Affine.IntLtForm -> NatValue
detIntLtForm :: IntLtForm -> NatValue
detIntLtForm (Affine.LtL NatValue
k IntTerm
_) = NatValue
k
detIntLtForm (Affine.LtR IntTerm
_ NatValue
k) = NatValue
k
detIntLtForm Affine.LtC{}     = NatValue
1

detIntDivForm :: Affine.IntDivForm -> NatValue
detIntDivForm :: IntDivForm -> NatValue
detIntDivForm (Affine.DivL NatValue
_ NatValue
k IntTerm
_) = NatValue
k
detIntDivForm Affine.DivC{}       = NatValue
1

detConjunct :: AffineDNFConjunct -> NatValue
detConjunct :: AffineDNFConjunct -> NatValue
detConjunct (Affine.IntLt IntLtForm
form) = IntLtForm -> NatValue
detIntLtForm IntLtForm
form
detConjunct (Affine.IntDiv IntDivForm
form) = IntDivForm -> NatValue
detIntDivForm IntDivForm
form
detConjunct (Affine.IntNegDiv IntDivForm
form) = IntDivForm -> NatValue
detIntDivForm IntDivForm
form

detDisjunct :: AffineDNFDisjunct -> NatValue
detDisjunct :: AffineDNFDisjunct -> NatValue
detDisjunct = (NatValue -> AffineDNFConjunct -> NatValue)
-> NatValue -> AffineDNFDisjunct -> NatValue
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (\NatValue
acc AffineDNFConjunct
c -> NatValue -> NatValue -> NatValue
forall a. Integral a => a -> a -> a
lcm NatValue
acc (AffineDNFConjunct -> NatValue
detConjunct AffineDNFConjunct
c)) NatValue
1

normIntLtForm :: NatValue -> Affine.IntLtForm -> IntLtForm
normIntLtForm :: NatValue -> IntLtForm -> IntLtForm
normIntLtForm NatValue
det (Affine.LtL NatValue
k IntTerm
i) = IntTerm -> IntLtForm
LtL (IntValue -> IntTerm -> IntTerm
Term.mul (NatValue -> IntValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatValue
det NatValue -> NatValue -> NatValue
forall a. Integral a => a -> a -> a
`div` NatValue
k)) IntTerm
i)
normIntLtForm NatValue
det (Affine.LtR IntTerm
i NatValue
k) = IntTerm -> IntLtForm
LtR (IntValue -> IntTerm -> IntTerm
Term.mul (NatValue -> IntValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatValue
det NatValue -> NatValue -> NatValue
forall a. Integral a => a -> a -> a
`div` NatValue
k)) IntTerm
i)
normIntLtForm NatValue
_ (Affine.LtC IntTerm
i IntTerm
j)   = IntTerm -> IntTerm -> IntLtForm
LtC IntTerm
i IntTerm
j

normIntDivForm :: NatValue -> Affine.IntDivForm -> IntDivForm
normIntDivForm :: NatValue -> IntDivForm -> IntDivForm
normIntDivForm NatValue
det (Affine.DivL NatValue
h NatValue
k IntTerm
i) = NatValue -> IntTerm -> IntDivForm
DivL (NatValue
h NatValue -> NatValue -> NatValue
forall a. Num a => a -> a -> a
* (NatValue
det NatValue -> NatValue -> NatValue
forall a. Integral a => a -> a -> a
`div` NatValue
k)) (IntValue -> IntTerm -> IntTerm
Term.mul (NatValue -> IntValue
forall a b. (Integral a, Num b) => a -> b
fromIntegral (NatValue
det NatValue -> NatValue -> NatValue
forall a. Integral a => a -> a -> a
`div` NatValue
k)) IntTerm
i)
normIntDivForm NatValue
_ (Affine.DivC NatValue
h IntTerm
i) = NatValue -> IntTerm -> IntDivForm
DivC NatValue
h IntTerm
i

normConjunct :: NatValue -> AffineDNFConjunct -> NormAffineDNFConjunct
normConjunct :: NatValue -> AffineDNFConjunct -> NormAffineDNFConjunct
normConjunct NatValue
det (Affine.IntLt IntLtForm
form) = IntLtForm -> NormAffineDNFConjunct
IntLt (NatValue -> IntLtForm -> IntLtForm
normIntLtForm NatValue
det IntLtForm
form)
normConjunct NatValue
det (Affine.IntDiv IntDivForm
form) = IntDivForm -> NormAffineDNFConjunct
IntDiv (NatValue -> IntDivForm -> IntDivForm
normIntDivForm NatValue
det IntDivForm
form)
normConjunct NatValue
det (Affine.IntNegDiv IntDivForm
form) = IntDivForm -> NormAffineDNFConjunct
IntNegDiv (NatValue -> IntDivForm -> IntDivForm
normIntDivForm NatValue
det IntDivForm
form)

normDisjunct :: NatValue -> AffineDNFDisjunct -> NormAffineDNFDisjunct
normDisjunct :: NatValue -> AffineDNFDisjunct -> [NormAffineDNFConjunct]
normDisjunct NatValue
det AffineDNFDisjunct
c = IntDivForm -> NormAffineDNFConjunct
IntDiv (NatValue -> IntTerm -> IntDivForm
DivL NatValue
det (IntValue -> IntTerm
IntConst IntValue
0)) NormAffineDNFConjunct
-> [NormAffineDNFConjunct] -> [NormAffineDNFConjunct]
forall a. a -> [a] -> [a]
: (AffineDNFConjunct -> NormAffineDNFConjunct)
-> AffineDNFDisjunct -> [NormAffineDNFConjunct]
forall a b. (a -> b) -> [a] -> [b]
map (NatValue -> AffineDNFConjunct -> NormAffineDNFConjunct
normConjunct NatValue
det) AffineDNFDisjunct
c

fromAffineDNF :: AffineDNF -> NormAffineDNF
fromAffineDNF :: AffineDNF -> NormAffineDNF
fromAffineDNF = (AffineDNFDisjunct -> [NormAffineDNFConjunct])
-> AffineDNF -> NormAffineDNF
forall a b. (a -> b) -> [a] -> [b]
map (\AffineDNFDisjunct
d -> NatValue -> AffineDNFDisjunct -> [NormAffineDNFConjunct]
normDisjunct (AffineDNFDisjunct -> NatValue
detDisjunct AffineDNFDisjunct
d) AffineDNFDisjunct
d)