{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Eta reduce" #-}
module Hermod.ReCon.Presburger.Formula(BinRel(..), Formula(..), unfoldImplies) where

import           Hermod.ReCon.Common.Types (BinRel (..), NatValue)
import           Hermod.ReCon.Integer.Polynomial.Term

-- | Formulae of Presburger arithmetic — the first-order theory of the integers
--   under addition (@+@), integer constants, and the standard comparison
--   relations (@=@, @<@, @≤@, @>@, @≥@), extended with the divisibility
--   predicate @d | t@ ("@d@ divides @t@").
--
--   Quantifiers range over ℤ only.  There are no free variables: every
--   well-formed formula is a closed sentence whose truth value is decidable
--   via Cooper's quantifier-elimination procedure
--   ('Hermod.ReCon.Presburger.Decide.decide').
data Formula =
     -- | φ ∨ ψ
     Or Formula Formula
     -- | φ ∧ ψ
   | And Formula Formula
     -- | ¬ φ
   | Not Formula
     -- | φ ⇒ ψ
   | Implies Formula Formula
     -- | T
   | Top
     -- | ⊥
   | Bottom
     -- | ∀x : ℤ. φ
   | IntForall VariableIdentifier Formula
     -- | ∃x : ℤ. φ
   | IntExists VariableIdentifier Formula
     -- | 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 -> Formula -> ShowS
[Formula] -> ShowS
Formula -> String
(Int -> Formula -> ShowS)
-> (Formula -> String) -> ([Formula] -> ShowS) -> Show Formula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Formula -> ShowS
showsPrec :: Int -> Formula -> ShowS
$cshow :: Formula -> String
show :: Formula -> String
$cshowList :: [Formula] -> ShowS
showList :: [Formula] -> ShowS
Show, Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
/= :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula =>
(Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
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 :: Formula -> Formula -> Ordering
compare :: Formula -> Formula -> Ordering
$c< :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
>= :: Formula -> Formula -> Bool
$cmax :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
min :: Formula -> Formula -> Formula
Ord)

unfoldImplies :: Formula -> Formula -> Formula
unfoldImplies :: Formula -> Formula -> Formula
unfoldImplies Formula
a Formula
b = Formula -> Formula -> Formula
Or (Formula -> Formula
Not Formula
a) Formula
b