{- HLINT ignore "Use <$>" -}
{- HLINT ignore "Use newtype instead of data" -}
module Hermod.ReCon.LTL.Formula.Parser (Parser, Context(..), Domain(..), PropKind(..), text, name, formula) where


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

import           Prelude hiding (head)

import           Control.Monad (guard)
import           Data.Char (isAlpha, isAlphaNum)
import           Data.Foldable (asum)
import           Data.Functor (void, (<&>))
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Text (Text)
import qualified Data.Text as Text
import           GHC.Unicode (isControl, isSpace)
import           Text.Megaparsec
import           Text.Megaparsec.Char (char, space, string)
import           Text.Megaparsec.Char.Lexer (decimal)

-- | The kind of a property variable: integer or text.
data PropKind = IntKind | TextKind deriving (Int -> PropKind -> ShowS
[PropKind] -> ShowS
PropKind -> String
(Int -> PropKind -> ShowS)
-> (PropKind -> String) -> ([PropKind] -> ShowS) -> Show PropKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PropKind -> ShowS
showsPrec :: Int -> PropKind -> ShowS
$cshow :: PropKind -> String
show :: PropKind -> String
$cshowList :: [PropKind] -> ShowS
showList :: [PropKind] -> ShowS
Show, PropKind -> PropKind -> Bool
(PropKind -> PropKind -> Bool)
-> (PropKind -> PropKind -> Bool) -> Eq PropKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PropKind -> PropKind -> Bool
== :: PropKind -> PropKind -> Bool
$c/= :: PropKind -> PropKind -> Bool
/= :: PropKind -> PropKind -> Bool
Eq, Eq PropKind
Eq PropKind =>
(PropKind -> PropKind -> Ordering)
-> (PropKind -> PropKind -> Bool)
-> (PropKind -> PropKind -> Bool)
-> (PropKind -> PropKind -> Bool)
-> (PropKind -> PropKind -> Bool)
-> (PropKind -> PropKind -> PropKind)
-> (PropKind -> PropKind -> PropKind)
-> Ord PropKind
PropKind -> PropKind -> Bool
PropKind -> PropKind -> Ordering
PropKind -> PropKind -> PropKind
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 :: PropKind -> PropKind -> Ordering
compare :: PropKind -> PropKind -> Ordering
$c< :: PropKind -> PropKind -> Bool
< :: PropKind -> PropKind -> Bool
$c<= :: PropKind -> PropKind -> Bool
<= :: PropKind -> PropKind -> Bool
$c> :: PropKind -> PropKind -> Bool
> :: PropKind -> PropKind -> Bool
$c>= :: PropKind -> PropKind -> Bool
>= :: PropKind -> PropKind -> Bool
$cmax :: PropKind -> PropKind -> PropKind
max :: PropKind -> PropKind -> PropKind
$cmin :: PropKind -> PropKind -> PropKind
min :: PropKind -> PropKind -> PropKind
Ord)

-- | A typed domain for a property variable.
data Domain = IntDomain (Set IntValue) | TextDomain (Set Text) deriving (Int -> Domain -> ShowS
[Domain] -> ShowS
Domain -> String
(Int -> Domain -> ShowS)
-> (Domain -> String) -> ([Domain] -> ShowS) -> Show Domain
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Domain -> ShowS
showsPrec :: Int -> Domain -> ShowS
$cshow :: Domain -> String
show :: Domain -> String
$cshowList :: [Domain] -> ShowS
showList :: [Domain] -> ShowS
Show, Domain -> Domain -> Bool
(Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool) -> Eq Domain
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Domain -> Domain -> Bool
== :: Domain -> Domain -> Bool
$c/= :: Domain -> Domain -> Bool
/= :: Domain -> Domain -> Bool
Eq, Eq Domain
Eq Domain =>
(Domain -> Domain -> Ordering)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Bool)
-> (Domain -> Domain -> Domain)
-> (Domain -> Domain -> Domain)
-> Ord Domain
Domain -> Domain -> Bool
Domain -> Domain -> Ordering
Domain -> Domain -> Domain
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 :: Domain -> Domain -> Ordering
compare :: Domain -> Domain -> Ordering
$c< :: Domain -> Domain -> Bool
< :: Domain -> Domain -> Bool
$c<= :: Domain -> Domain -> Bool
<= :: Domain -> Domain -> Bool
$c> :: Domain -> Domain -> Bool
> :: Domain -> Domain -> Bool
$c>= :: Domain -> Domain -> Bool
>= :: Domain -> Domain -> Bool
$cmax :: Domain -> Domain -> Domain
max :: Domain -> Domain -> Domain
$cmin :: Domain -> Domain -> Domain
min :: Domain -> Domain -> Domain
Ord)

data Context = Context {
  Context -> [(Text, Domain)]
interpDomain :: [(Text, Domain)],
  -- | Kinds of in-scope property variables, populated by quantifier parsers.
  Context -> Map Text PropKind
varKinds     :: Map VariableIdentifier PropKind
}

isSubscriptDigit :: Char -> Bool
isSubscriptDigit :: Char -> Bool
isSubscriptDigit Char
c = Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
>= Char
'₀' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Ord a => a -> a -> Bool
<= Char
'₉'

unescapedVariableIdentifierNextChar :: Parser Char
unescapedVariableIdentifierNextChar :: Parser Char
unescapedVariableIdentifierNextChar = (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
x -> Char -> Bool
isAlphaNum Char
Token Text
x Bool -> Bool -> Bool
|| Char
Token Text
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char -> Bool
isSubscriptDigit Char
Token Text
x)

unescapedVariableIdentifier :: Parser Text
unescapedVariableIdentifier :: Parser Text
unescapedVariableIdentifier =
  String -> Text
Text.pack (String -> Text)
-> ParsecT Void Text Identity String -> Parser Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) (Char -> ShowS) -> Parser Char -> ParsecT Void Text Identity ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
firstChar ParsecT Void Text Identity ShowS
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
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 Char -> ParsecT Void Text Identity String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Char
unescapedVariableIdentifierNextChar) Parser Text -> String -> Parser Text
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"identifier" where
  firstChar :: Parser Char
  firstChar :: Parser Char
firstChar = (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
x -> Char -> Bool
isAlpha Char
Token Text
x Bool -> Bool -> Bool
|| Char
Token Text
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_')

superscriptDigit :: Parser Word
superscriptDigit :: Parser Word
superscriptDigit = Word
0 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
1 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
2 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
3 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
4 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
5 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
6 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
7 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
8 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
9 Word -> Parser Char -> Parser Word
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
<$ 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
'⁹'

subscriptDigit :: Parser Word
subscriptDigit :: Parser Word
subscriptDigit = Word
0 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
1 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
2 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
3 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
4 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
5 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
6 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
7 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
8 Word -> Parser Char -> Parser Word
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
<$ 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 Word -> Parser Word -> Parser Word
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
<|> Word
9 Word -> Parser Char -> Parser Word
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
<$ 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
'₉'

littleEndian :: Word -> [Word] -> Word
littleEndian :: Word -> [Word] -> Word
littleEndian Word
radix = Word -> Word -> [Word] -> Word
go Word
0 Word
1 where
  go :: Word -> Word -> [Word] -> Word
  go :: Word -> Word -> [Word] -> Word
go Word
acc Word
_ []            = Word
acc
  go Word
acc Word
factor (Word
d : [Word]
ds) = Word -> Word -> [Word] -> Word
go (Word
acc Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
d Word -> Word -> Word
forall a. Num a => a -> a -> a
* Word
factor) (Word
radix Word -> Word -> Word
forall a. Num a => a -> a -> a
* Word
factor) [Word]
ds

bigEndian :: Word -> [Word] -> Word
bigEndian :: Word -> [Word] -> Word
bigEndian Word
radix = Word -> [Word] -> Word
littleEndian Word
radix ([Word] -> Word) -> ([Word] -> [Word]) -> [Word] -> Word
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word] -> [Word]
forall a. [a] -> [a]
reverse

asciiIndexing :: Parser Word
asciiIndexing :: Parser Word
asciiIndexing = 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 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 Word -> Parser Word
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 Word
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
decimal Parser Word -> ParsecT Void Text Identity () -> Parser Word
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 Word -> Parser Char -> Parser Word
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
')'

superscriptWord :: Parser Word
superscriptWord :: Parser Word
superscriptWord = Word -> [Word] -> Word
bigEndian Word
10 ([Word] -> Word)
-> ParsecT Void Text Identity [Word] -> Parser Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Word -> ParsecT Void Text Identity [Word]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Word
superscriptDigit Parser Word -> Parser Word -> Parser Word
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 Word
asciiIndexing

subscriptWord :: Parser Word
subscriptWord :: Parser Word
subscriptWord = Word -> [Word] -> Word
bigEndian Word
10 ([Word] -> Word)
-> ParsecT Void Text Identity [Word] -> Parser Word
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Word -> ParsecT Void Text Identity [Word]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Word
subscriptDigit Parser Word -> Parser Word -> Parser Word
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 Word
asciiIndexing

variableIdentifier :: Parser Text
variableIdentifier :: Parser Text
variableIdentifier = Parser Text
unescapedVariableIdentifier

text :: Parser Text
text :: Parser Text
text = String -> Text
Text.pack (String -> Text)
-> ParsecT Void Text Identity String -> Parser Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
'\"' Parser Char
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
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 Char -> ParsecT Void Text Identity String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Char
one) Parser Text -> Parser Char -> Parser Text
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
'\"' where
  one :: Parser Char
  one :: Parser Char
one = (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
x -> Bool -> Bool
not (Char -> Bool
isControl Char
Token Text
x) Bool -> Bool -> Bool
&& (Bool -> Bool
not (Char -> Bool
isSpace Char
Token Text
x) Bool -> Bool -> Bool
|| Char
Token Text
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
' ') Bool -> Bool -> Bool
&& Char
Token Text
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'"')

-- | Unquoted name: [_a-zA-Z][_a-zA-Z0-9._]*  — for namespaces and property keys.
unquotedName :: Parser Text
unquotedName :: Parser Text
unquotedName =
  String -> Text
Text.pack (String -> Text)
-> ParsecT Void Text Identity String -> Parser Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) (Char -> ShowS) -> Parser Char -> ParsecT Void Text Identity ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
ParsecT Void Text Identity (Token Text)
firstChar ParsecT Void Text Identity ShowS
-> ParsecT Void Text Identity String
-> ParsecT Void Text Identity String
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 Char -> ParsecT Void Text Identity String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Char
ParsecT Void Text Identity (Token Text)
nextChar) Parser Text -> String -> Parser Text
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"name"
  where
    firstChar :: ParsecT Void Text Identity (Token Text)
firstChar = (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
c -> Char -> Bool
isAlpha Char
Token Text
c Bool -> Bool -> Bool
|| Char
Token Text
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_')
    nextChar :: ParsecT Void Text Identity (Token Text)
nextChar  = (Token Text -> Bool) -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (\Token Text
c -> Char -> Bool
isAlphaNum Char
Token Text
c Bool -> Bool -> Bool
|| Char
Token Text
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
Token Text
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.')

-- | A name is either an unquoted identifier or a quoted string.
name :: Parser Text
name :: Parser Text
name = Parser Text -> Parser Text
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 Text
unquotedName Parser Text -> Parser Text -> Parser 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
<|> Parser Text
text

formulaBottom :: Parser (Formula event ty)
formulaBottom :: forall event ty. Parser (Formula event ty)
formulaBottom = Formula event ty
forall event ty. Formula event ty
Bottom Formula event ty
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Formula event ty)
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
<$ (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 (Formula event ty)
formulaTop :: forall event ty. Parser (Formula event ty)
formulaTop = Formula event ty
forall event ty. Formula event ty
Top Formula event ty
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Formula event ty)
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
<$ (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")

-- | Parse a single property constraint inside an Atom: "propname" = term.
--   The term kind is determined by the RHS: int literal → IntPropConstraint,
--   text literal → TextPropConstraint, variable → look up kind in ctx.varKinds.
constraint :: Context -> Parser PropConstraint
constraint :: Context -> Parser PropConstraint
constraint Context
ctx = do
  Text
propName <- Parser Text
name Parser Text -> ParsecT Void Text Identity () -> Parser Text
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 Text -> Parser Char -> Parser Text
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
'='
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  (Text -> IntTerm -> PropConstraint
IntPropConstraint  Text
propName (IntTerm -> PropConstraint)
-> (IntValue -> IntTerm) -> IntValue -> PropConstraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntValue -> IntTerm
IntConst (IntValue -> PropConstraint)
-> ParsecT Void Text Identity IntValue -> Parser PropConstraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity IntValue
-> ParsecT Void Text Identity IntValue
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 ParsecT Void Text Identity IntValue
parseIntValue)
    Parser PropConstraint
-> Parser PropConstraint -> Parser PropConstraint
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
<|> (Text -> TextTerm -> PropConstraint
TextPropConstraint Text
propName (TextTerm -> PropConstraint)
-> (Text -> TextTerm) -> Text -> PropConstraint
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> TextTerm
TextConst (Text -> PropConstraint) -> Parser Text -> Parser PropConstraint
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
text)
    Parser PropConstraint
-> Parser PropConstraint -> Parser PropConstraint
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
<|> do
          Text
var <- Parser Text
variableIdentifier
          case Text -> Map Text PropKind -> Maybe PropKind
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
var Context
ctx.varKinds of
            Just PropKind
IntKind  -> PropConstraint -> Parser PropConstraint
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PropConstraint -> Parser PropConstraint)
-> PropConstraint -> Parser PropConstraint
forall a b. (a -> b) -> a -> b
$ Text -> IntTerm -> PropConstraint
IntPropConstraint  Text
propName (IntValue -> Text -> IntTerm
IntVar IntValue
1 Text
var)
            Just PropKind
TextKind -> PropConstraint -> Parser PropConstraint
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PropConstraint -> Parser PropConstraint)
-> PropConstraint -> Parser PropConstraint
forall a b. (a -> b) -> a -> b
$ Text -> TextTerm -> PropConstraint
TextPropConstraint Text
propName (Text -> TextTerm
TextVar Text
var)
            Maybe PropKind
Nothing       -> String -> Parser PropConstraint
forall a. String -> ParsecT Void Text Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser PropConstraint)
-> String -> Parser PropConstraint
forall a b. (a -> b) -> a -> b
$ String
"Unknown variable kind for: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
Text.unpack Text
var

constraints :: Context -> Parser (Set PropConstraint)
constraints :: Context -> Parser (Set PropConstraint)
constraints Context
ctx = [PropConstraint] -> Set PropConstraint
forall a. Ord a => [a] -> Set a
Set.fromList ([PropConstraint] -> Set PropConstraint)
-> ParsecT Void Text Identity [PropConstraint]
-> Parser (Set PropConstraint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
'{' Parser 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 ()
-> ParsecT Void Text Identity [PropConstraint]
-> ParsecT Void Text Identity [PropConstraint]
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 PropConstraint
-> Parser Char -> ParsecT Void Text Identity [PropConstraint]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (Context -> Parser PropConstraint
constraint Context
ctx) (ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Char -> Parser Char
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
*> 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 Char -> ParsecT Void Text Identity () -> Parser Char
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 [PropConstraint]
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity [PropConstraint]
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 [PropConstraint]
-> Parser Char -> ParsecT Void Text Identity [PropConstraint]
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
'}')

formulaInParens :: Context -> Parser ty -> Parser (Formula event ty)
formulaInParens :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaInParens Context
ctx Parser ty
ty = 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 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 ()
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUniverse Context
ctx Parser ty
ty ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
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 (Formula event ty)
-> Parser Char -> ParsecT Void Text Identity (Formula event ty)
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
')'

formulaPropAtom :: Context -> Parser ty -> Parser (Formula event ty)
formulaPropAtom :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPropAtom Context
ctx Parser ty
ty = ty -> Set PropConstraint -> Formula event ty
forall event ty. ty -> Set PropConstraint -> Formula event ty
Atom (ty -> Set PropConstraint -> Formula event ty)
-> Parser ty
-> ParsecT
     Void Text Identity (Set PropConstraint -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ty
ty ParsecT Void Text Identity (Set PropConstraint -> Formula event ty)
-> Parser (Set PropConstraint)
-> ParsecT Void Text Identity (Formula event ty)
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
<*> (ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity ()
-> Parser (Set PropConstraint) -> Parser (Set PropConstraint)
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
*> Context -> Parser (Set PropConstraint)
constraints Context
ctx)

formulaAtom :: Context -> Parser ty -> Parser (Formula event ty)
formulaAtom :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty = Parser (Formula event ty)
forall event ty. Parser (Formula event ty)
formulaBottom Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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 event ty)
forall event ty. Parser (Formula event ty)
formulaTop Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaInParens Context
ctx Parser ty
ty Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPropAtom Context
ctx Parser ty
ty

formulaTemporalNextOp :: Parser ()
formulaTemporalNextOp :: ParsecT Void Text Identity ()
formulaTemporalNextOp = 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
"\\next"

formulaTemporalExistsOp :: Parser ()
formulaTemporalExistsOp :: ParsecT Void Text Identity ()
formulaTemporalExistsOp = 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
"\\finallyN"

formulaTemporalForallOp :: Parser ()
formulaTemporalForallOp :: ParsecT Void Text Identity ()
formulaTemporalForallOp = 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
"\\globallyN"

formulaTemporalForallInfOp :: Parser ()
formulaTemporalForallInfOp :: ParsecT Void Text Identity ()
formulaTemporalForallInfOp = 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
<|> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity (Tokens Text)
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 (Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
"\\globally" ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Tokens Text)
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
<* Parser Char -> ParsecT Void Text Identity ()
forall a.
ParsecT Void Text Identity a -> ParsecT Void Text Identity ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy (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
'N'))

formulaNext :: Context -> Parser ty -> Parser (Formula event ty)
formulaNext :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNext Context
ctx Parser ty
ty = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Next (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity ()
formulaTemporalNextOp 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 ()
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty)

formulaNextN :: Context -> Parser ty -> Parser (Formula event ty)
formulaNextN :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNextN Context
ctx Parser ty
ty = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
NextN (Word -> Formula event ty -> Formula event ty)
-> Parser Word
-> ParsecT
     Void Text Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Word -> Parser Word
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 (ParsecT Void Text Identity ()
formulaTemporalNextOp ParsecT Void Text Identity () -> Parser Word -> Parser Word
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 Word
superscriptWord) Parser Word -> ParsecT Void Text Identity () -> Parser Word
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 (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty

formulaExistsN :: Context -> Parser ty -> Parser (Formula event ty)
formulaExistsN :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaExistsN Context
ctx Parser ty
ty = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ExistsN (Word -> Formula event ty -> Formula event ty)
-> Parser Word
-> ParsecT
     Void Text Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity ()
formulaTemporalExistsOp ParsecT Void Text Identity () -> Parser Word -> Parser Word
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 Word
superscriptWord Parser Word -> ParsecT Void Text Identity () -> Parser Word
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 (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty

formulaForallN :: Context -> Parser ty -> Parser (Formula event ty)
formulaForallN :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaForallN Context
ctx Parser ty
ty = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
ForallN (Word -> Formula event ty -> Formula event ty)
-> Parser Word
-> ParsecT
     Void Text Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity ()
formulaTemporalForallOp ParsecT Void Text Identity () -> Parser Word -> Parser Word
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 Word
superscriptWord Parser Word -> ParsecT Void Text Identity () -> Parser Word
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 (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty

formulaForall :: Context -> Parser ty -> Parser (Formula event ty)
formulaForall :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaForall Context
ctx Parser ty
ty = Word -> Formula event ty -> Formula event ty
forall event ty. Word -> Formula event ty -> Formula event ty
Forall (Word -> Formula event ty -> Formula event ty)
-> Parser Word
-> ParsecT
     Void Text Identity (Formula event ty -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ParsecT Void Text Identity ()
formulaTemporalForallInfOp ParsecT Void Text Identity () -> Parser Word -> Parser Word
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
*> Word -> Parser Word -> Parser Word
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
option Word
0 Parser Word
subscriptWord Parser Word -> ParsecT Void Text Identity () -> Parser Word
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 (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty

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"

formulaNot :: Context -> Parser ty -> Parser (Formula event ty)
formulaNot :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNot Context
ctx Parser ty
ty = Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
Not (Formula event ty -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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 ()
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
*> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty)

-- | Set of int values from a literal {1, 2, 3}.
setIntConst :: Parser (Set IntValue)
setIntConst :: Parser (Set IntValue)
setIntConst = [IntValue] -> Set IntValue
forall a. Ord a => [a] -> Set a
Set.fromList ([IntValue] -> Set IntValue)
-> ParsecT Void Text Identity [IntValue] -> Parser (Set IntValue)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
'{' Parser 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 ()
-> ParsecT Void Text Identity [IntValue]
-> ParsecT Void Text Identity [IntValue]
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 IntValue
-> Parser Char -> ParsecT Void Text Identity [IntValue]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy ParsecT Void Text Identity IntValue
parseIntValue (ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Char -> Parser Char
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
*> 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 Char -> ParsecT Void Text Identity () -> Parser Char
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 [IntValue]
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity [IntValue]
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 [IntValue]
-> Parser Char -> ParsecT Void Text Identity [IntValue]
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
'}')

-- | Set of text values from a literal {"a", "b"}.
setTextConst :: Parser (Set Text)
setTextConst :: Parser (Set Text)
setTextConst = [Text] -> Set Text
forall a. Ord a => [a] -> Set a
Set.fromList ([Text] -> Set Text)
-> ParsecT Void Text Identity [Text] -> Parser (Set Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
'{' Parser 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 ()
-> ParsecT Void Text Identity [Text]
-> ParsecT Void Text Identity [Text]
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 Text -> Parser Char -> ParsecT Void Text Identity [Text]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Text
text (ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space ParsecT Void Text Identity () -> Parser Char -> Parser Char
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
*> 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 Char -> ParsecT Void Text Identity () -> Parser Char
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 [Text]
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity [Text]
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 [Text]
-> Parser Char -> ParsecT Void Text Identity [Text]
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
'}')

-- | A domain literal: try int first (so {1,2,3} is Int, not Text), then text.
setDomainConst :: Parser Domain
setDomainConst :: Parser Domain
setDomainConst = (Set IntValue -> Domain
IntDomain (Set IntValue -> Domain) -> Parser (Set IntValue) -> Parser Domain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Set IntValue) -> Parser (Set IntValue)
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 (Set IntValue)
setIntConst) Parser Domain -> Parser Domain -> Parser Domain
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
<|> (Set Text -> Domain
TextDomain (Set Text -> Domain) -> Parser (Set Text) -> Parser Domain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Set Text)
setTextConst)

-- | A domain variable resolved from the context (prefixed by $).
setDomainVar :: Context -> Parser Domain
setDomainVar :: Context -> Parser Domain
setDomainVar Context
ctx = do
  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
"$"
  [Parser Domain] -> Parser Domain
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum (Context
ctx.interpDomain [(Tokens Text, Domain)]
-> ((Tokens Text, Domain) -> Parser Domain) -> [Parser Domain]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Tokens Text
k, Domain
v) -> Domain
v Domain -> ParsecT Void Text Identity (Tokens Text) -> Parser Domain
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
<$ Tokens Text -> ParsecT Void Text Identity (Tokens Text)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens Text
k)

setDomain :: Context -> Parser Domain
setDomain :: Context -> Parser Domain
setDomain Context
ctx = Context -> Parser Domain
setDomainVar Context
ctx Parser Domain -> Parser Domain -> Parser Domain
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 Domain
setDomainConst

-- | Parse an integer or text binary-relation atom.
--   LHS may be an int literal or a variable identifier; RHS likewise.
--   Text equality (x = "s") is the only form that produces PropTextEq.
formulaEq :: Context -> Parser ty -> Parser (Formula event ty)
formulaEq :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaEq Context
ctx Parser ty
ty =
  ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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 (do
    Either IntValue Text
lhs <- IntValue -> Either IntValue Text
forall a b. a -> Either a b
Left (IntValue -> Either IntValue Text)
-> ParsecT Void Text Identity IntValue
-> ParsecT Void Text Identity (Either IntValue Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity IntValue
-> ParsecT Void Text Identity IntValue
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 ParsecT Void Text Identity IntValue
parseIntValue ParsecT Void Text Identity (Either IntValue Text)
-> ParsecT Void Text Identity (Either IntValue Text)
-> ParsecT Void Text Identity (Either IntValue 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
<|> Text -> Either IntValue Text
forall a b. b -> Either a b
Right (Text -> Either IntValue Text)
-> Parser Text -> ParsecT Void Text Identity (Either IntValue Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
variableIdentifier
    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
    case Either IntValue Text
lhs of
      Right Text
x ->
              BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
rel Relevance event ty
forall a. Set a
Set.empty (IntValue -> Text -> IntTerm
IntVar IntValue
1 Text
x) (IntTerm -> Formula event ty)
-> ParsecT Void Text Identity IntTerm
-> ParsecT Void Text Identity (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity IntTerm
-> ParsecT Void Text Identity IntTerm
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 ParsecT Void Text Identity IntTerm
intTerm
          ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<|> Bool -> ParsecT Void Text Identity ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (BinRel
rel BinRel -> BinRel -> Bool
forall a. Eq a => a -> a -> Bool
== BinRel
Eq) ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
*> (Relevance event ty -> TextTerm -> Text -> Formula event ty
forall event ty.
Relevance event ty -> TextTerm -> Text -> Formula event ty
PropTextEq Relevance event ty
forall a. Set a
Set.empty (Text -> TextTerm
TextVar Text
x) (Text -> Formula event ty)
-> Parser Text -> ParsecT Void Text Identity (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text
text)
      Left IntValue
v ->
        BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
forall event ty.
BinRel
-> Relevance event ty -> IntTerm -> IntTerm -> Formula event ty
PropIntBinRel BinRel
rel Relevance event ty
forall a. Set a
Set.empty (IntValue -> IntTerm
IntConst IntValue
v) (IntTerm -> Formula event ty)
-> ParsecT Void Text Identity IntTerm
-> ParsecT Void Text Identity (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity IntTerm
intTerm
  )
  ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
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
<|> Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAtom Context
ctx Parser ty
ty

formulaPrefixOrEq :: Context -> Parser ty -> Parser (Formula event ty)
formulaPrefixOrEq :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPrefixOrEq Context
ctx Parser ty
ty =
      Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNextN Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNext Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaExistsN Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaForall Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaForallN Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaNot Context
ctx Parser ty
ty
  Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaEq Context
ctx Parser ty
ty

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
"&&"

formulaAnd :: Context -> Parser ty -> Parser (Formula event ty)
formulaAnd :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAnd Context
ctx Parser ty
ty = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply (Formula event ty -> Maybe (Formula event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT
     Void Text Identity (Maybe (Formula event ty) -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPrefixOrEq Context
ctx Parser ty
ty ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
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 event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
-> ParsecT Void Text Identity (Formula event ty)
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
<*> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
    ParsecT Void Text Identity ()
formulaAndOp
    ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
    Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAnd Context
ctx Parser ty
ty) where
  apply :: Formula event ty -> Maybe (Formula event ty) -> Formula event ty
  apply :: forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply Formula event ty
phi Maybe (Formula event ty)
Nothing     = Formula event ty
phi
  apply Formula event ty
phi (Just !Formula event ty
psi) = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
And Formula event ty
phi Formula event ty
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
"||"

formulaOr :: Context -> Parser ty -> Parser (Formula event ty)
formulaOr :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaOr Context
ctx Parser ty
ty = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply (Formula event ty -> Maybe (Formula event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT
     Void Text Identity (Maybe (Formula event ty) -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaAnd Context
ctx Parser ty
ty ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
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 event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
-> ParsecT Void Text Identity (Formula event ty)
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
<*> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
    ParsecT Void Text Identity ()
formulaOrOp
    ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
    Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaOr Context
ctx Parser ty
ty) where
  apply :: Formula event ty -> Maybe (Formula event ty) -> Formula event ty
  apply :: forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply Formula event ty
phi Maybe (Formula event ty)
Nothing     = Formula event ty
phi
  apply Formula event ty
phi (Just !Formula event ty
psi) = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Or Formula event ty
phi Formula event ty
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
"=>"

formulaImplies :: Context -> Parser ty -> Parser (Formula event ty)
formulaImplies :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaImplies Context
ctx Parser ty
ty = Formula event ty -> Maybe (Formula event ty) -> Formula event ty
forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply (Formula event ty -> Maybe (Formula event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT
     Void Text Identity (Maybe (Formula event ty) -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaOr Context
ctx Parser ty
ty ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
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 event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
-> ParsecT Void Text Identity (Formula event ty)
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
<*> ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity (Maybe (Formula event ty))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
    ParsecT Void Text Identity ()
formulaImpliesOp
    ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
    Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaImplies Context
ctx Parser ty
ty) where
  apply :: Formula event ty -> Maybe (Formula event ty) -> Formula event ty
  apply :: forall event ty.
Formula event ty -> Maybe (Formula event ty) -> Formula event ty
apply Formula event ty
phi Maybe (Formula event ty)
Nothing     = Formula event ty
phi
  apply Formula event ty
phi (Just !Formula event ty
psi) = Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Formula event ty -> Formula event ty -> Formula event ty
Implies Formula event ty
phi Formula event ty
psi

data Quantifier = Universal | Existential

formulaIntKind :: Parser ()
formulaIntKind :: ParsecT Void Text Identity ()
formulaIntKind = 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
"\\Int" 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
"Int"

formulaTextKind :: Parser ()
formulaTextKind :: ParsecT Void Text Identity ()
formulaTextKind = 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
"\\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
"Text"

-- | Handles Qx ∈ ℤ. φ,  Qx ∈ Text. φ,  Qx ∈ dom. φ  where Q is ∀ or ∃
formulaPropQuantifier :: Context -> Parser ty -> Parser (Formula event ty)
formulaPropQuantifier :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPropQuantifier Context
ctx Parser ty
ty = do
  Quantifier
q <- ParsecT Void Text Identity Quantifier
-> ParsecT Void Text Identity Quantifier
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 (ParsecT Void Text Identity Quantifier
 -> ParsecT Void Text Identity Quantifier)
-> ParsecT Void Text Identity Quantifier
-> ParsecT Void Text Identity Quantifier
forall a b. (a -> b) -> a -> b
$
        (Quantifier
Universal   Quantifier
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity Quantifier
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
<$ (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")) ParsecT Void Text Identity Quantifier
-> ParsecT Void Text Identity Quantifier
-> ParsecT Void Text Identity Quantifier
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
<|>
        (Quantifier
Existential Quantifier
-> ParsecT Void Text Identity (Tokens Text)
-> ParsecT Void Text Identity Quantifier
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
<$ (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"))
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Text
x <- Parser Text
variableIdentifier
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  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
":"
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  Either PropKind Domain
result <-
    (PropKind -> Either PropKind Domain
forall a b. a -> Either a b
Left  (PropKind -> Either PropKind Domain)
-> ParsecT Void Text Identity PropKind
-> ParsecT Void Text Identity (Either PropKind Domain)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (PropKind
IntKind PropKind
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity PropKind
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 ()
formulaIntKind ParsecT Void Text Identity PropKind
-> ParsecT Void Text Identity PropKind
-> ParsecT Void Text Identity PropKind
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
<|> PropKind
TextKind PropKind
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity PropKind
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 ()
formulaTextKind))
    ParsecT Void Text Identity (Either PropKind Domain)
-> ParsecT Void Text Identity (Either PropKind Domain)
-> ParsecT Void Text Identity (Either PropKind Domain)
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
<|>
    (Domain -> Either PropKind Domain
forall a b. b -> Either a b
Right (Domain -> Either PropKind Domain)
-> Parser Domain
-> ParsecT Void Text Identity (Either PropKind Domain)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Parser Domain
setDomain Context
ctx)
  ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  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 ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
  let (PropKind
kind, Formula event ty -> Formula event ty
ctor) = case (Quantifier
q, Either PropKind Domain
result) of
        (Quantifier
Universal,   Left PropKind
IntKind)          -> (PropKind
IntKind,  Text -> Formula event ty -> Formula event ty
forall event ty. Text -> Formula event ty -> Formula event ty
PropIntForall  Text
x)
        (Quantifier
Universal,   Left PropKind
TextKind)         -> (PropKind
TextKind, Text -> Formula event ty -> Formula event ty
forall event ty. Text -> Formula event ty -> Formula event ty
PropTextForall Text
x)
        (Quantifier
Universal,   Right (IntDomain  Set IntValue
is)) -> (PropKind
IntKind,  Text -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
Text -> Set IntValue -> Formula event ty -> Formula event ty
PropIntForallN  Text
x Set IntValue
is)
        (Quantifier
Universal,   Right (TextDomain Set Text
ts)) -> (PropKind
TextKind, Text -> Set Text -> Formula event ty -> Formula event ty
forall event ty.
Text -> Set Text -> Formula event ty -> Formula event ty
PropTextForallN Text
x Set Text
ts)
        (Quantifier
Existential, Left PropKind
IntKind)          -> (PropKind
IntKind,  Text -> Formula event ty -> Formula event ty
forall event ty. Text -> Formula event ty -> Formula event ty
PropIntExists  Text
x)
        (Quantifier
Existential, Left PropKind
TextKind)         -> (PropKind
TextKind, Text -> Formula event ty -> Formula event ty
forall event ty. Text -> Formula event ty -> Formula event ty
PropTextExists Text
x)
        (Quantifier
Existential, Right (IntDomain  Set IntValue
is)) -> (PropKind
IntKind,  Text -> Set IntValue -> Formula event ty -> Formula event ty
forall event ty.
Text -> Set IntValue -> Formula event ty -> Formula event ty
PropIntExistsN  Text
x Set IntValue
is)
        (Quantifier
Existential, Right (TextDomain Set Text
ts)) -> (PropKind
TextKind, Text -> Set Text -> Formula event ty -> Formula event ty
forall event ty.
Text -> Set Text -> Formula event ty -> Formula event ty
PropTextExistsN Text
x Set Text
ts)
  Formula event ty -> Formula event ty
forall event ty. Formula event ty -> Formula event ty
ctor (Formula event ty -> Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUniverse (Context
ctx { varKinds = Map.insert x kind ctx.varKinds }) Parser ty
ty

formulaUntilN :: Context -> Parser ty -> Parser (Formula event ty)
formulaUntilN :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUntilN Context
ctx Parser ty
ty = Formula event ty
-> Maybe (Word, Formula event ty) -> Formula event ty
forall event ty.
Formula event ty
-> Maybe (Word, Formula event ty) -> Formula event ty
apply (Formula event ty
 -> Maybe (Word, Formula event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Formula event ty)
-> ParsecT
     Void
     Text
     Identity
     (Maybe (Word, Formula event ty) -> Formula event ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaImplies Context
ctx Parser ty
ty ParsecT Void Text Identity (Formula event ty)
-> ParsecT Void Text Identity ()
-> ParsecT Void Text Identity (Formula event ty)
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 (Word, Formula event ty) -> Formula event ty)
-> ParsecT Void Text Identity (Maybe (Word, Formula event ty))
-> ParsecT Void Text Identity (Formula event ty)
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
<*> ParsecT Void Text Identity (Word, Formula event ty)
-> ParsecT Void Text Identity (Maybe (Word, Formula event ty))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (do
     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
"|"
     Word
k <- Parser Word
superscriptWord
     ParsecT Void Text Identity ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space
     Formula event ty
phi <- Context
-> Parser ty -> ParsecT Void Text Identity (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaImplies Context
ctx Parser ty
ty
     (Word, Formula event ty)
-> ParsecT Void Text Identity (Word, Formula event ty)
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word
k, Formula event ty
phi)) where
  apply :: Formula event ty -> Maybe (Word, Formula event ty) -> Formula event ty
  apply :: forall event ty.
Formula event ty
-> Maybe (Word, Formula event ty) -> Formula event ty
apply Formula event ty
phi Maybe (Word, Formula event ty)
Nothing           = Formula event ty
phi
  apply Formula event ty
phi (Just (!Word
k, !Formula event ty
psi)) = Word -> Formula event ty -> Formula event ty -> Formula event ty
forall event ty.
Word -> Formula event ty -> Formula event ty -> Formula event ty
UntilN Word
k Formula event ty
phi Formula event ty
psi

formulaUniverse :: Context -> Parser ty -> Parser (Formula event ty)
formulaUniverse :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUniverse Context
ctx Parser ty
ty = Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaPropQuantifier Context
ctx Parser ty
ty
                     Parser (Formula event ty)
-> Parser (Formula event ty) -> Parser (Formula event ty)
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
<|> Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUntilN Context
ctx Parser ty
ty

formula :: Context -> Parser ty -> Parser (Formula event ty)
formula :: forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formula = Context -> Parser ty -> Parser (Formula event ty)
forall ty event. Context -> Parser ty -> Parser (Formula event ty)
formulaUniverse