{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use <$>" #-}
module Hermod.ReCon.Presburger.Parser (Parser, formula, intTerm) where

import           Hermod.ReCon.Common.Parser
import           Hermod.ReCon.Common.Types
import           Hermod.ReCon.Integer.Polynomial.Parser (intTerm)
import           Hermod.ReCon.Presburger.Formula (Formula (..))

import           Data.Functor (void)
import           Text.Megaparsec
import           Text.Megaparsec.Char (char, space, string)

-- ---------------------------------------------------------------------------
-- Formula parser
-- ---------------------------------------------------------------------------

-- | @d ∣ t@: divisibility constraint.  @d@ must be a non-zero nat.
intDivConstraint :: Parser Formula
intDivConstraint :: Parser Formula
intDivConstraint = do
  NatValue
d <- Parser NatValue
parseNatValue
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity Char -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'∣'
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  IntTerm
t <- Parser IntTerm
intTerm
  Formula -> Parser Formula
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NatValue -> IntTerm -> Formula
IntDiv NatValue
d IntTerm
t)

-- | @t₁ rel t₂@: binary relation constraint.
intRelConstraint :: Parser Formula
intRelConstraint :: Parser Formula
intRelConstraint = do
  IntTerm
lhs <- Parser IntTerm
intTerm
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  BinRel
rel <- Parser BinRel
parseBinRel
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  IntTerm
rhs <- Parser IntTerm
intTerm
  Formula -> Parser Formula
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BinRel -> IntTerm -> IntTerm -> Formula
IntBinRel BinRel
rel IntTerm
lhs IntTerm
rhs)

formulaBottom :: Parser ()
formulaBottom :: ParsecT Void Text Identity ()
formulaBottom = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"⊥" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\bottom"

formulaTop :: Parser ()
formulaTop :: ParsecT Void Text Identity ()
formulaTop = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"⊤" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\top"

-- | Atom: ⊥, ⊤, parenthesised formula, or an arithmetic constraint.
formulaAtom :: Parser Formula
formulaAtom :: Parser Formula
formulaAtom =
      Formula
Bottom Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ParsecT Void Text Identity ()
formulaBottom
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Formula
Top    Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ParsecT Void Text Identity ()
formulaTop
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'(' ParsecT Void Text Identity Char
-> ParsecT Void Text Identity () -> ParsecT Void Text Identity ()
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Formula -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Formula
formula Parser Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space Parser Formula -> ParsecT Void Text Identity Char -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
')')
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Formula
intDivConstraint
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Formula
intRelConstraint

formulaNotOp :: Parser ()
formulaNotOp :: ParsecT Void Text Identity ()
formulaNotOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"¬" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\not"

-- | Prefix negation applied to a single atom.
formulaNot :: Parser Formula
formulaNot :: Parser Formula
formulaNot =
      Formula -> Formula
Not (Formula -> Formula) -> Parser Formula -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity ()
formulaNotOp ParsecT Void Text Identity ()
-> ParsecT Void Text Identity () -> ParsecT Void Text Identity ()
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Formula -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Formula
formulaAtom)
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Formula
formulaAtom

formulaAndOp :: Parser ()
formulaAndOp :: ParsecT Void Text Identity ()
formulaAndOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"∧" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"&&"

-- | Right-associative conjunction @φ ∧ ψ@.
formulaAnd :: Parser Formula
formulaAnd :: Parser Formula
formulaAnd = Formula -> Maybe Formula -> Formula
apply (Formula -> Maybe Formula -> Formula)
-> Parser Formula
-> ParsecT Void Text Identity (Maybe Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Formula
formulaNot Parser Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space) ParsecT Void Text Identity (Maybe Formula -> Formula)
-> ParsecT Void Text Identity (Maybe Formula) -> Parser Formula
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Formula -> ParsecT Void Text Identity (Maybe Formula)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser Formula
rhs
  where
    rhs :: Parser Formula
rhs = ParsecT Void Text Identity ()
formulaAndOp ParsecT Void Text Identity ()
-> ParsecT Void Text Identity () -> ParsecT Void Text Identity ()
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Formula -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Formula
formulaAnd
    apply :: Formula -> Maybe Formula -> Formula
apply Formula
phi Maybe Formula
Nothing    = Formula
phi
    apply Formula
phi (Just Formula
psi) = Formula -> Formula -> Formula
And Formula
phi Formula
psi

formulaOrOp :: Parser ()
formulaOrOp :: ParsecT Void Text Identity ()
formulaOrOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"∨" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"||"

-- | Right-associative disjunction @φ ∨ ψ@.
formulaOr :: Parser Formula
formulaOr :: Parser Formula
formulaOr = Formula -> Maybe Formula -> Formula
apply (Formula -> Maybe Formula -> Formula)
-> Parser Formula
-> ParsecT Void Text Identity (Maybe Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Formula
formulaAnd Parser Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space) ParsecT Void Text Identity (Maybe Formula -> Formula)
-> ParsecT Void Text Identity (Maybe Formula) -> Parser Formula
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Formula -> ParsecT Void Text Identity (Maybe Formula)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser Formula
rhs
  where
    rhs :: Parser Formula
rhs = ParsecT Void Text Identity ()
formulaOrOp ParsecT Void Text Identity ()
-> ParsecT Void Text Identity () -> ParsecT Void Text Identity ()
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Formula -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Formula
formulaOr
    apply :: Formula -> Maybe Formula -> Formula
apply Formula
phi Maybe Formula
Nothing    = Formula
phi
    apply Formula
phi (Just Formula
psi) = Formula -> Formula -> Formula
Or Formula
phi Formula
psi

formulaImpliesOp :: Parser ()
formulaImpliesOp :: ParsecT Void Text Identity ()
formulaImpliesOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"⇒" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"=>"

-- | Right-associative implication @φ ⇒ ψ@.
formulaImplies :: Parser Formula
formulaImplies :: Parser Formula
formulaImplies = Formula -> Maybe Formula -> Formula
apply (Formula -> Maybe Formula -> Formula)
-> Parser Formula
-> ParsecT Void Text Identity (Maybe Formula -> Formula)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Formula
formulaOr Parser Formula -> ParsecT Void Text Identity () -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space) ParsecT Void Text Identity (Maybe Formula -> Formula)
-> ParsecT Void Text Identity (Maybe Formula) -> Parser Formula
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Formula -> ParsecT Void Text Identity (Maybe Formula)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser Formula
rhs
  where
    rhs :: Parser Formula
rhs = ParsecT Void Text Identity ()
formulaImpliesOp ParsecT Void Text Identity ()
-> ParsecT Void Text Identity () -> ParsecT Void Text Identity ()
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Formula -> Parser Formula
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Formula
formulaImplies
    apply :: Formula -> Maybe Formula -> Formula
apply Formula
phi Maybe Formula
Nothing    = Formula
phi
    apply Formula
phi (Just Formula
psi) = Formula -> Formula -> Formula
Implies Formula
phi Formula
psi

formulaForallOp :: Parser ()
formulaForallOp :: ParsecT Void Text Identity ()
formulaForallOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"∀" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\forall"

-- | @∀x. φ@: universal integer quantification.
formulaForall :: Parser Formula
formulaForall :: Parser Formula
formulaForall = do
  ParsecT Void Text Identity ()
formulaForallOp
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Text
x <- Parser Text
parseIdentifier
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity Char -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'.'
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Formula
phi <- Parser Formula
formula
  Formula -> Parser Formula
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Formula -> Formula
IntForall Text
x Formula
phi)

formulaExistsOp :: Parser ()
formulaExistsOp :: ParsecT Void Text Identity ()
formulaExistsOp = ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity (Tokens Text)
 -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"∃" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\exists"

-- | @∃x. φ@: existential integer quantification.
formulaExists :: Parser Formula
formulaExists :: Parser Formula
formulaExists = do
  ParsecT Void Text Identity ()
formulaExistsOp
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Text
x <- Parser Text
parseIdentifier
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT Void Text Identity Char -> ParsecT Void Text Identity ())
-> ParsecT Void Text Identity Char -> ParsecT Void Text Identity ()
forall a b. (a -> b) -> a -> b
$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'.'
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Formula
phi <- Parser Formula
formula
  Formula -> Parser Formula
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text -> Formula -> Formula
IntExists Text
x Formula
phi)

-- | Parse a Presburger arithmetic formula.
--
-- Precedence table (outermost / lowest binding first):
--
-- @
--   ∀x. φ   ∃x. φ     quantifiers
--   φ ⇒ ψ             implication (right-associative)
--   φ ∨ ψ             disjunction (right-associative)
--   φ ∧ ψ             conjunction (right-associative)
--   ¬ φ               negation    (prefix, binds to single atom)
--   ⊥  ⊤  (φ)  d∣t  t rel t     atoms
-- @
--
-- Note: to combine a quantifier with a connective write
-- @φ ∧ (∀x. ψ)@ — quantifiers inside sub-formulas must be parenthesised.
formula :: Parser Formula
formula :: Parser Formula
formula =
      Parser Formula
formulaForall
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Formula
formulaExists
  Parser Formula -> Parser Formula -> Parser Formula
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Formula
formulaImplies