module Hermod.ReCon.Presburger.Internal.IR.ForallFree (ForallFree(..), fromFormula) where

import           Hermod.ReCon.Common.Types (NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term
import           Hermod.ReCon.Presburger.Formula (BinRel)
import qualified Hermod.ReCon.Presburger.Formula as C

-- | Presburger formulae with all universal quantifiers eliminated by duality:
--   @∀x. φ  ≡  ¬(∃x. ¬φ)@.
--   Only existential quantifiers remain; the structure is otherwise identical
--   to 'Hermod.ReCon.Presburger.Formula.Formula'.
--   This is the first IR in the Cooper QE pipeline.
data ForallFree =
     -- | φ ∨ ψ
     Or ForallFree ForallFree
     -- | φ ∧ ψ
   | And ForallFree ForallFree
     -- | ¬ φ
   | Not ForallFree
     -- | φ ⇒ ψ
   | Implies ForallFree ForallFree
     -- | T
   | Top
     -- | ⊥
   | Bottom
     -- | ∃x ∈ ℤ. φ
   | IntExists VariableIdentifier ForallFree
     -- | i = i | i < i | i ≤ i | i > i | i ≥ i
   | IntBinRel BinRel IntTerm IntTerm
     -- | ℕ⁺ \| i  (divisibility relation, first argument is a non-zero ℕ)
   | IntDiv NatValue IntTerm
   deriving (Int -> ForallFree -> ShowS
[ForallFree] -> ShowS
ForallFree -> String
(Int -> ForallFree -> ShowS)
-> (ForallFree -> String)
-> ([ForallFree] -> ShowS)
-> Show ForallFree
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ForallFree -> ShowS
showsPrec :: Int -> ForallFree -> ShowS
$cshow :: ForallFree -> String
show :: ForallFree -> String
$cshowList :: [ForallFree] -> ShowS
showList :: [ForallFree] -> ShowS
Show, ForallFree -> ForallFree -> Bool
(ForallFree -> ForallFree -> Bool)
-> (ForallFree -> ForallFree -> Bool) -> Eq ForallFree
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ForallFree -> ForallFree -> Bool
== :: ForallFree -> ForallFree -> Bool
$c/= :: ForallFree -> ForallFree -> Bool
/= :: ForallFree -> ForallFree -> Bool
Eq, Eq ForallFree
Eq ForallFree =>
(ForallFree -> ForallFree -> Ordering)
-> (ForallFree -> ForallFree -> Bool)
-> (ForallFree -> ForallFree -> Bool)
-> (ForallFree -> ForallFree -> Bool)
-> (ForallFree -> ForallFree -> Bool)
-> (ForallFree -> ForallFree -> ForallFree)
-> (ForallFree -> ForallFree -> ForallFree)
-> Ord ForallFree
ForallFree -> ForallFree -> Bool
ForallFree -> ForallFree -> Ordering
ForallFree -> ForallFree -> ForallFree
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 :: ForallFree -> ForallFree -> Ordering
compare :: ForallFree -> ForallFree -> Ordering
$c< :: ForallFree -> ForallFree -> Bool
< :: ForallFree -> ForallFree -> Bool
$c<= :: ForallFree -> ForallFree -> Bool
<= :: ForallFree -> ForallFree -> Bool
$c> :: ForallFree -> ForallFree -> Bool
> :: ForallFree -> ForallFree -> Bool
$c>= :: ForallFree -> ForallFree -> Bool
>= :: ForallFree -> ForallFree -> Bool
$cmax :: ForallFree -> ForallFree -> ForallFree
max :: ForallFree -> ForallFree -> ForallFree
$cmin :: ForallFree -> ForallFree -> ForallFree
min :: ForallFree -> ForallFree -> ForallFree
Ord)

-- | Eliminate all universal quantifiers via  ∀x. φ  ≡  ¬(∃x. ¬φ).
fromFormula :: C.Formula -> ForallFree
fromFormula :: Formula -> ForallFree
fromFormula (C.Or Formula
a Formula
b)          = ForallFree -> ForallFree -> ForallFree
Or (Formula -> ForallFree
fromFormula Formula
a) (Formula -> ForallFree
fromFormula Formula
b)
fromFormula (C.And Formula
a Formula
b)         = ForallFree -> ForallFree -> ForallFree
And (Formula -> ForallFree
fromFormula Formula
a) (Formula -> ForallFree
fromFormula Formula
b)
fromFormula (C.Not Formula
a)           = ForallFree -> ForallFree
Not (Formula -> ForallFree
fromFormula Formula
a)
fromFormula (C.Implies Formula
a Formula
b)     = ForallFree -> ForallFree -> ForallFree
Implies (Formula -> ForallFree
fromFormula Formula
a) (Formula -> ForallFree
fromFormula Formula
b)
fromFormula Formula
C.Top               = ForallFree
Top
fromFormula Formula
C.Bottom            = ForallFree
Bottom
fromFormula (C.IntExists VariableIdentifier
x Formula
φ)   = VariableIdentifier -> ForallFree -> ForallFree
IntExists VariableIdentifier
x (Formula -> ForallFree
fromFormula Formula
φ)
fromFormula (C.IntForall VariableIdentifier
x Formula
φ)   = ForallFree -> ForallFree
Not (VariableIdentifier -> ForallFree -> ForallFree
IntExists VariableIdentifier
x (ForallFree -> ForallFree
Not (Formula -> ForallFree
fromFormula Formula
φ)))
fromFormula (C.IntBinRel BinRel
r IntTerm
i IntTerm
j) = BinRel -> IntTerm -> IntTerm -> ForallFree
IntBinRel BinRel
r IntTerm
i IntTerm
j
fromFormula (C.IntDiv NatValue
k IntTerm
t)      = NatValue -> IntTerm -> ForallFree
IntDiv NatValue
k IntTerm
t