{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}

-- |
-- Module       : Data.TPTP.Parse.Combinators
-- Description  : Parser combinators for the TPTP language.
-- Copyright    : (c) Evgenii Kotelnikov, 2019-2021
-- License      : GPL-3
-- Maintainer   : evgeny.kotelnikov@gmail.com
-- Stability    : experimental
--

module Data.TPTP.Parse.Combinators (
  -- * Whitespace
  skipWhitespace,
  input,

  -- * Names
  atom,
  var,
  distinctObject,
  function,
  predicate,

  -- * Sorts and types
  sort,
  tff1Sort,
  type_,

  -- * First-order logic
  number,
  term,
  literal,
  clause,
  unsortedFirstOrder,
  sortedFirstOrder,
  monomorphicFirstOrder,
  polymorphicFirstOrder,

  -- * Units
  unit,
  tptp,
  tstp,

  -- * Annotations
  szs,
  intro,
  parent,
  source,
  info
) where

#if MIN_VERSION_base(4, 8, 0)
import Prelude hiding (pure, (<$>), (<*>), (*>), (<*))
#endif

import Control.Applicative (pure, (<*>), (*>), (<*), (<|>), optional, empty, many)
import Data.Char (isAscii, isAsciiLower, isAsciiUpper, isDigit, isPrint)
import Data.Function (on)
import Data.Functor ((<$>), ($>))
import Data.Maybe (fromMaybe)
#if !MIN_VERSION_base(4, 8, 0)
import Data.Monoid (Monoid(..))
#endif
import Data.List (sortBy, genericLength)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NEL (fromList, toList)
#if !MIN_VERSION_base(4, 11, 0)
import Data.Semigroup (Semigroup(..), sconcat)
#else
import Data.Semigroup (sconcat)
#endif

import qualified Data.Scientific as Sci (base10Exponent, coefficient)

import Data.Text (Text)
import qualified Data.Text as Text (pack, unpack, cons)

import Data.Attoparsec.Text as Atto (
    Parser,
    (<?>), char, string, decimal, scientific, signed, isEndOfLine, endOfLine,
    satisfy, option, eitherP, choice, manyTill, takeWhile, skip, skipSpace,
    skipMany, skipWhile, endOfInput, sepBy, sepBy1
  )

import Data.TPTP hiding (name, clause)
import qualified Data.TPTP as TPTP (name)


-- * Helper functions

-- | Consume all character until the end of line.
skipLine :: Parser ()
skipLine :: Parser ()
skipLine = (Char -> Bool) -> Parser ()
skipWhile (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isEndOfLine)
{-# INLINE skipLine #-}

-- | Consume the first character of a single line comment - @%@ or @#@.
-- The grammar of the TPTP language only defines @%@,
-- but some theorem provers in addition use @#@.
skipBeginComment :: Parser ()
skipBeginComment :: Parser ()
skipBeginComment = (Char -> Bool) -> Parser ()
skip (\Char
c -> Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'%' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'#')
{-# INLINE skipBeginComment #-}

-- | Parse the contents of a single line comment.
commented :: Parser p -> Parser p
commented :: Parser p -> Parser p
commented Parser p
p =  Parser ()
skipBeginComment Parser () -> Parser p -> Parser p
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser p
p Parser p -> Parser () -> Parser p
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipLine Parser p -> Parser () -> Parser p
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser ()
endOfLine Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
forall t. Chunk t => Parser t ()
endOfInput)
           Parser p -> String -> Parser p
forall i a. Parser i a -> String -> Parser i a
<?> String
"commented"

-- | Consume a single line comment - characters between @%@ or @#@ and newline.
skipComment :: Parser ()
skipComment :: Parser ()
skipComment = Parser () -> Parser ()
forall p. Parser p -> Parser p
commented (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Parser () -> String -> Parser ()
forall i a. Parser i a -> String -> Parser i a
<?> String
"comment"
{-# INLINE skipComment #-}

-- | Consume a block comment - characters between /* and */.
skipBlockComment :: Parser ()
skipBlockComment :: Parser ()
skipBlockComment = Text -> Parser Text
string Text
"/*" Parser Text -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
bc Parser () -> String -> Parser ()
forall i a. Parser i a -> String -> Parser i a
<?> String
"block comment"
  where
    bc :: Parser ()
bc = (Char -> Bool) -> Parser ()
skipWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'*') Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Parser Text
string Text
"*/" Parser Text -> () -> Parser ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> () Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
bc)

-- | Consume white space and trailing comments.
skipWhitespace :: Parser ()
skipWhitespace :: Parser ()
skipWhitespace =  Parser ()
skipSpace
               Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f ()
skipMany ((Parser ()
skipComment Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
skipBlockComment) Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace)
              Parser () -> String -> Parser ()
forall i a. Parser i a -> String -> Parser i a
<?> String
"whitespace"

-- | @lexeme@ makes a given parser consume trailing whitespace. This function is
-- needed because off-the-shelf attoparsec parsers do not do it.
lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme Parser a
p = Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipWhitespace
{-# INLINE lexeme #-}

-- | @input@ runs a given parser skipping leading whitespace. The function
-- succeeds if the parser consumes the entire input.
input :: Parser a -> Parser a
input :: Parser a -> Parser a
input Parser a
p = Parser ()
skipWhitespace Parser () -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall t. Chunk t => Parser t ()
endOfInput Parser a -> String -> Parser a
forall i a. Parser i a -> String -> Parser i a
<?> String
"input"
{-# INLINE input #-}

-- | Parse an unsigned integer.
integer :: Parser Integer
integer :: Parser Integer
integer = Parser Integer -> Parser Integer
forall p. Parser p -> Parser p
lexeme Parser Integer
forall a. Integral a => Parser a
decimal Parser Integer -> String -> Parser Integer
forall i a. Parser i a -> String -> Parser i a
<?> String
"integer"
{-# INLINE integer #-}

token :: Text -> Parser Text
token :: Text -> Parser Text
token Text
t = Parser Text -> Parser Text
forall p. Parser p -> Parser p
lexeme (Text -> Parser Text
string Text
t) Parser Text -> String -> Parser Text
forall i a. Parser i a -> String -> Parser i a
<?> String
"token " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
t
{-# INLINE token #-}

op :: Char -> Parser Char
op :: Char -> Parser Char
op Char
c = Parser Char -> Parser Char
forall p. Parser p -> Parser p
lexeme (Char -> Parser Char
char Char
c) Parser Char -> String -> Parser Char
forall i a. Parser i a -> String -> Parser i a
<?> String
"operator " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
c]
{-# INLINE op #-}

parens :: Parser a -> Parser a
parens :: Parser a -> Parser a
parens Parser a
p = Char -> Parser Char
op Char
'(' Parser Char -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser Char -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
')' Parser a -> String -> Parser a
forall i a. Parser i a -> String -> Parser i a
<?> String
"parens"
{-# INLINE parens #-}

optionalParens :: Parser a -> Parser a
optionalParens :: Parser a -> Parser a
optionalParens Parser a
p = Parser a
p Parser a -> Parser a -> Parser a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a -> Parser a
forall p. Parser p -> Parser p
parens (Parser a -> Parser a
forall p. Parser p -> Parser p
optionalParens Parser a
p)
{-# INLINE optionalParens #-}

brackets :: Parser a -> Parser a
brackets :: Parser a -> Parser a
brackets Parser a
p = Char -> Parser Char
op Char
'[' Parser Char -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser Char -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
']' Parser a -> String -> Parser a
forall i a. Parser i a -> String -> Parser i a
<?> String
"brackets"
{-# INLINE brackets #-}

bracketList :: Parser a -> Parser [a]
bracketList :: Parser a -> Parser [a]
bracketList Parser a
p = Parser [a] -> Parser [a]
forall p. Parser p -> Parser p
brackets (Parser a
p Parser a -> Parser Char -> Parser [a]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy` Char -> Parser Char
op Char
',') Parser [a] -> String -> Parser [a]
forall i a. Parser i a -> String -> Parser i a
<?> String
"bracket list"
{-# INLINE bracketList #-}

bracketList1 :: Parser a -> Parser (NonEmpty a)
bracketList1 :: Parser a -> Parser (NonEmpty a)
bracketList1 Parser a
p =  [a] -> NonEmpty a
forall a. [a] -> NonEmpty a
NEL.fromList ([a] -> NonEmpty a) -> Parser Text [a] -> Parser (NonEmpty a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text [a] -> Parser Text [a]
forall p. Parser p -> Parser p
brackets (Parser a
p Parser a -> Parser Char -> Parser Text [a]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy1` Char -> Parser Char
op Char
',')
              Parser (NonEmpty a) -> String -> Parser (NonEmpty a)
forall i a. Parser i a -> String -> Parser i a
<?> String
"bracket list 1"
{-# INLINE bracketList1 #-}

application :: Parser f -> Parser a -> Parser (f, [a])
application :: Parser f -> Parser a -> Parser (f, [a])
application Parser f
f Parser a
a = (,) (f -> [a] -> (f, [a])) -> Parser f -> Parser Text ([a] -> (f, [a]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser f
f Parser Text ([a] -> (f, [a])) -> Parser Text [a] -> Parser (f, [a])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> Parser Text [a] -> Parser Text [a]
forall (f :: * -> *) a. Alternative f => a -> f a -> f a
option [] (Parser Text [a] -> Parser Text [a]
forall p. Parser p -> Parser p
parens (Parser a -> Parser a
forall p. Parser p -> Parser p
optionalParens Parser a
a Parser a -> Parser Char -> Parser Text [a]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy1` Char -> Parser Char
op Char
','))
{-# INLINE application #-}

labeled :: Text -> Parser a -> Parser a
labeled :: Text -> Parser a -> Parser a
labeled Text
l Parser a
p = Text -> Parser Text
token Text
l Parser Text -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser a
forall p. Parser p -> Parser p
parens Parser a
p
{-# INLINE labeled #-}

comma :: Parser a -> Parser a
comma :: Parser a -> Parser a
comma Parser a
p = Char -> Parser Char
op Char
',' Parser Char -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p
{-# INLINE comma #-}

maybeP :: Parser a -> Parser (Maybe a)
maybeP :: Parser a -> Parser (Maybe a)
maybeP = Parser a -> Parser (Maybe a)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser a -> Parser (Maybe a))
-> (Parser a -> Parser a) -> Parser a -> Parser (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser a -> Parser a
forall p. Parser p -> Parser p
comma
{-# INLINE maybeP #-}

named :: (Named a, Enum a, Bounded a) => Parser a
named :: Parser a
named = [Parser a] -> Parser a
forall (f :: * -> *) a. Alternative f => [f a] -> f a
choice
      ([Parser a] -> Parser a) -> [Parser a] -> Parser a
forall a b. (a -> b) -> a -> b
$ ((Text, a) -> Parser a) -> [(Text, a)] -> [Parser a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Text
n, a
c) -> Text -> Parser Text
string Text
n Parser Text -> a -> Parser a
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> a
c Parser a -> String -> Parser a
forall i a. Parser i a -> String -> Parser i a
<?> String
"named " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
Text.unpack Text
n)
      ([(Text, a)] -> [Parser a]) -> [(Text, a)] -> [Parser a]
forall a b. (a -> b) -> a -> b
$ ((Text, a) -> (Text, a) -> Ordering) -> [(Text, a)] -> [(Text, a)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Text -> Text -> Ordering) -> Text -> Text -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Text -> Text -> Ordering)
-> ((Text, a) -> Text) -> (Text, a) -> (Text, a) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Text, a) -> Text
forall a b. (a, b) -> a
fst)
      ([(Text, a)] -> [(Text, a)]) -> [(Text, a)] -> [(Text, a)]
forall a b. (a -> b) -> a -> b
$ (a -> (Text, a)) -> [a] -> [(Text, a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a
c -> (a -> Text
forall a. Named a => a -> Text
TPTP.name a
c, a
c)) [a
forall a. Bounded a => a
minBound..]

enum :: (Named a, Enum a, Bounded a) => Parser a
enum :: Parser a
enum = Parser a -> Parser a
forall p. Parser p -> Parser p
lexeme Parser a
forall a. (Named a, Enum a, Bounded a) => Parser a
named
{-# INLINE enum #-}


-- * Parser combinators

-- ** Names

isAlphaNumeric :: Char -> Bool
isAlphaNumeric :: Char -> Bool
isAlphaNumeric Char
c = Char -> Bool
isAsciiLower Char
c Bool -> Bool -> Bool
|| Char -> Bool
isAsciiUpper Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

isAsciiPrint :: Char -> Bool
isAsciiPrint :: Char -> Bool
isAsciiPrint Char
c = Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isPrint Char
c

lowerWord, upperWord :: Parser Text
lowerWord :: Parser Text
lowerWord = Char -> Text -> Text
Text.cons (Char -> Text -> Text) -> Parser Char -> Parser Text (Text -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Char
satisfy Char -> Bool
isAsciiLower Parser Text (Text -> Text) -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Char -> Bool) -> Parser Text
Atto.takeWhile Char -> Bool
isAlphaNumeric
upperWord :: Parser Text
upperWord = Char -> Text -> Text
Text.cons (Char -> Text -> Text) -> Parser Char -> Parser Text (Text -> Text)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser Char
satisfy Char -> Bool
isAsciiUpper Parser Text (Text -> Text) -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Char -> Bool) -> Parser Text
Atto.takeWhile Char -> Bool
isAlphaNumeric

quoted :: Char -> Parser Text
quoted :: Char -> Parser Text
quoted Char
q =  String -> Text
Text.pack (String -> Text) -> Parser Text String -> Parser Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Parser Char
char Char
q Parser Char -> Parser Text String -> Parser Text String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser Char -> Parser Text String
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
manyTill Parser Char
escaped (Char -> Parser Char
char Char
q))
        Parser Text -> String -> Parser Text
forall i a. Parser i a -> String -> Parser i a
<?> String
"quoted " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
q]
  where
    escaped :: Parser Char
escaped =  Char -> Parser Char
char Char
'\\' Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Char -> Parser Char
char Char
q Parser Char -> Char -> Parser Char
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Char
q Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Parser Char
char Char
'\\' Parser Char -> Char -> Parser Char
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Char
'\\')
           Parser Char -> Parser Char -> Parser Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Bool) -> Parser Char
satisfy Char -> Bool
isAsciiPrint

-- | Parse an atomic word. Single-quoted atoms are parsed without the single
-- quotes and with the characters @'@ and @\\@ unescaped.
atom :: Parser Atom
atom :: Parser Atom
atom = Text -> Atom
Atom (Text -> Atom) -> Parser Text -> Parser Atom
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser Text
forall p. Parser p -> Parser p
lexeme (Char -> Parser Text
quoted Char
'\'' Parser Text -> Parser Text -> Parser Text
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Text
lowerWord) Parser Atom -> String -> Parser Atom
forall i a. Parser i a -> String -> Parser i a
<?> String
"atom"
{-# INLINE atom #-}

-- | Parse a variable.
var :: Parser Var
var :: Parser Var
var = Text -> Var
Var (Text -> Var) -> Parser Text -> Parser Var
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser Text
forall p. Parser p -> Parser p
lexeme Parser Text
upperWord Parser Var -> String -> Parser Var
forall i a. Parser i a -> String -> Parser i a
<?> String
"var"
{-# INLINE var #-}

-- | Parse a distinct object. Double quotes are not preserved and the characters
-- @'@ and @\\@ are unescaped.
distinctObject :: Parser DistinctObject
distinctObject :: Parser DistinctObject
distinctObject = Text -> DistinctObject
DistinctObject (Text -> DistinctObject) -> Parser Text -> Parser DistinctObject
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser Text
forall p. Parser p -> Parser p
lexeme (Char -> Parser Text
quoted Char
'"') Parser DistinctObject -> String -> Parser DistinctObject
forall i a. Parser i a -> String -> Parser i a
<?> String
"distinct object"
{-# INLINE distinctObject #-}

-- | Parse a reserved word.
reserved :: (Named a, Enum a, Bounded a) => Parser (Reserved a)
reserved :: Parser (Reserved a)
reserved = Text -> Reserved a
forall a. (Named a, Enum a, Bounded a) => Text -> Reserved a
extended (Text -> Reserved a) -> Parser Text -> Parser (Reserved a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser Text
forall p. Parser p -> Parser p
lexeme Parser Text
lowerWord Parser (Reserved a) -> String -> Parser (Reserved a)
forall i a. Parser i a -> String -> Parser i a
<?> String
"reserved"
{-# INLINE reserved #-}

name :: (Named a, Enum a, Bounded a) => Parser (Name a)
name :: Parser (Name a)
name =  Reserved a -> Name a
forall s. Reserved s -> Name s
Reserved (Reserved a -> Name a)
-> Parser Text (Reserved a) -> Parser (Name a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Parser Char
char Char
'$' Parser Char -> Parser Text (Reserved a) -> Parser Text (Reserved a)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Text (Reserved a)
forall a. (Named a, Enum a, Bounded a) => Parser (Reserved a)
reserved)
    Parser (Name a) -> Parser (Name a) -> Parser (Name a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Atom -> Name a
forall s. Atom -> Name s
Defined  (Atom -> Name a) -> Parser Atom -> Parser (Name a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom
    Parser (Name a) -> String -> Parser (Name a)
forall i a. Parser i a -> String -> Parser i a
<?> String
"name"

-- | Parse a function name.
function :: Parser (Name Function)
function :: Parser (Name Function)
function = Parser (Name Function)
forall a. (Named a, Enum a, Bounded a) => Parser (Name a)
name Parser (Name Function) -> String -> Parser (Name Function)
forall i a. Parser i a -> String -> Parser i a
<?> String
"function"
{-# INLINE function #-}

-- | Parse a predicate name.
predicate :: Parser (Name Predicate)
predicate :: Parser (Name Predicate)
predicate = Parser (Name Predicate)
forall a. (Named a, Enum a, Bounded a) => Parser (Name a)
name Parser (Name Predicate) -> String -> Parser (Name Predicate)
forall i a. Parser i a -> String -> Parser i a
<?> String
"predicate"
{-# INLINE predicate #-}


-- ** Sorts and typess

-- | Parse a sort.
sort :: Parser (Name Sort)
sort :: Parser (Name Sort)
sort = Parser (Name Sort)
forall a. (Named a, Enum a, Bounded a) => Parser (Name a)
name Parser (Name Sort) -> String -> Parser (Name Sort)
forall i a. Parser i a -> String -> Parser i a
<?> String
"sort"
{-# INLINE sort #-}

-- | Parse a sort in sorted polymorphic logic.
tff1Sort :: Parser TFF1Sort
tff1Sort :: Parser TFF1Sort
tff1Sort =  Var -> TFF1Sort
SortVariable (Var -> TFF1Sort) -> Parser Var -> Parser TFF1Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
var
        Parser TFF1Sort -> Parser TFF1Sort -> Parser TFF1Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Name Sort -> [TFF1Sort] -> TFF1Sort)
-> (Name Sort, [TFF1Sort]) -> TFF1Sort
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name Sort -> [TFF1Sort] -> TFF1Sort
TFF1Sort ((Name Sort, [TFF1Sort]) -> TFF1Sort)
-> Parser Text (Name Sort, [TFF1Sort]) -> Parser TFF1Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Sort)
-> Parser TFF1Sort -> Parser Text (Name Sort, [TFF1Sort])
forall f a. Parser f -> Parser a -> Parser (f, [a])
application Parser (Name Sort)
sort Parser TFF1Sort
tff1Sort
        Parser TFF1Sort -> String -> Parser TFF1Sort
forall i a. Parser i a -> String -> Parser i a
<?> String
"tff1 sort"

mapping :: Parser a -> Parser ([a], a)
mapping :: Parser a -> Parser ([a], a)
mapping Parser a
s = (,) ([a] -> a -> ([a], a))
-> Parser Text [a] -> Parser Text (a -> ([a], a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a] -> Parser Text [a] -> Parser Text [a]
forall (f :: * -> *) a. Alternative f => a -> f a -> f a
option [] (Parser Text [a]
args Parser Text [a] -> Parser Char -> Parser Text [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
'>') Parser Text (a -> ([a], a)) -> Parser a -> Parser ([a], a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser a
s
  where
    args :: Parser Text [a]
args = (a -> [a]) -> Parser a -> Parser Text [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> [a] -> [a]
forall a. a -> [a] -> [a]
:[]) Parser a
s Parser Text [a] -> Parser Text [a] -> Parser Text [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Text [a] -> Parser Text [a]
forall p. Parser p -> Parser p
parens (Parser a
s Parser a -> Parser Char -> Parser Text [a]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy1` Char -> Parser Char
op Char
'*')

-- | Parse a type.
type_ :: Parser Type
type_ :: Parser Type
type_ =  ([TFF1Sort] -> TFF1Sort -> Type) -> ([TFF1Sort], TFF1Sort) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([TFF1Sort] -> TFF1Sort -> Type)
 -> ([TFF1Sort], TFF1Sort) -> Type)
-> ([Var] -> [TFF1Sort] -> TFF1Sort -> Type)
-> [Var]
-> ([TFF1Sort], TFF1Sort)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var] -> [TFF1Sort] -> TFF1Sort -> Type
tff1Type
     ([Var] -> ([TFF1Sort], TFF1Sort) -> Type)
-> Parser Text [Var]
-> Parser Text (([TFF1Sort], TFF1Sort) -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Var] -> (NonEmpty Var -> [Var]) -> Maybe (NonEmpty Var) -> [Var]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] NonEmpty Var -> [Var]
forall a. NonEmpty a -> [a]
NEL.toList (Maybe (NonEmpty Var) -> [Var])
-> Parser Text (Maybe (NonEmpty Var)) -> Parser Text [Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (NonEmpty Var) -> Parser Text (Maybe (NonEmpty Var))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser Text (NonEmpty Var)
prefix) Parser Text (([TFF1Sort], TFF1Sort) -> Type)
-> Parser Text ([TFF1Sort], TFF1Sort) -> Parser Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text ([TFF1Sort], TFF1Sort)
matrix
     Parser Type -> String -> Parser Type
forall i a. Parser i a -> String -> Parser i a
<?> String
"type"
  where
    prefix :: Parser Text (NonEmpty Var)
prefix = Text -> Parser Text
token Text
"!>" Parser Text
-> Parser Text (NonEmpty Var) -> Parser Text (NonEmpty Var)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Var -> Parser Text (NonEmpty Var)
forall a. Parser a -> Parser (NonEmpty a)
bracketList1 Parser Var
sortVar Parser Text (NonEmpty Var)
-> Parser Char -> Parser Text (NonEmpty Var)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
':'
    sortVar :: Parser Var
sortVar = Parser Var
var Parser Var -> Parser Char -> Parser Var
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
':' Parser Var -> Parser Text -> Parser Var
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Text -> Parser Text
forall p. Parser p -> Parser p
optionalParens (Text -> Parser Text
token Text
"$tType")
    matrix :: Parser Text ([TFF1Sort], TFF1Sort)
matrix = Parser Text ([TFF1Sort], TFF1Sort)
-> Parser Text ([TFF1Sort], TFF1Sort)
forall p. Parser p -> Parser p
optionalParens (Parser TFF1Sort -> Parser Text ([TFF1Sort], TFF1Sort)
forall a. Parser a -> Parser ([a], a)
mapping (Parser TFF1Sort -> Parser TFF1Sort
forall p. Parser p -> Parser p
optionalParens Parser TFF1Sort
tff1Sort))


-- ** First-order logic

-- | Parse a number.
number :: Parser Number
number :: Parser Number
number =  Integer -> Integer -> Number
RationalConstant (Integer -> Integer -> Number)
-> Parser Integer -> Parser Text (Integer -> Number)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer -> Parser Integer
forall a. Num a => Parser a -> Parser a
signed Parser Integer
integer Parser Text (Integer -> Number)
-> Parser Char -> Parser Text (Integer -> Number)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
char Char
'/' Parser Text (Integer -> Number) -> Parser Integer -> Parser Number
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer
integer
      Parser Number -> Parser Number -> Parser Number
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Scientific -> Number
real (Scientific -> Number) -> Parser Text Scientific -> Parser Number
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Scientific -> Parser Text Scientific
forall p. Parser p -> Parser p
lexeme Parser Text Scientific
scientific
      Parser Number -> String -> Parser Number
forall i a. Parser i a -> String -> Parser i a
<?> String
"number"
  where
    real :: Scientific -> Number
real Scientific
n
      | Scientific -> Int
Sci.base10Exponent Scientific
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer -> Number
IntegerConstant (Scientific -> Integer
Sci.coefficient Scientific
n)
      | Bool
otherwise = Scientific -> Number
RealConstant Scientific
n

-- | Parse a term.
--
-- @term@ supports parsing superfluous parenthesis around arguments
-- of the function application, which are not present in the TPTP grammar.
term :: Parser Term
term :: Parser Term
term =  (Name Function -> [Term] -> Term)
-> (Name Function, [Term]) -> Term
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name Function -> [Term] -> Term
Function ((Name Function, [Term]) -> Term)
-> Parser Text (Name Function, [Term]) -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Function)
-> Parser Term -> Parser Text (Name Function, [Term])
forall f a. Parser f -> Parser a -> Parser (f, [a])
application Parser (Name Function)
function Parser Term
term
    Parser Term -> Parser Term -> Parser Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var -> Term
Variable         (Var -> Term) -> Parser Var -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
var
    Parser Term -> Parser Term -> Parser Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Number -> Term
Number           (Number -> Term) -> Parser Number -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Number
number
    Parser Term -> Parser Term -> Parser Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DistinctObject -> Term
DistinctTerm     (DistinctObject -> Term) -> Parser DistinctObject -> Parser Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser DistinctObject
distinctObject
    Parser Term -> String -> Parser Term
forall i a. Parser i a -> String -> Parser i a
<?> String
"term"

-- | Parse the equality and the inequality sign.
eq :: Parser Sign
eq :: Parser Sign
eq = Parser Sign
forall a. (Named a, Enum a, Bounded a) => Parser a
enum Parser Sign -> String -> Parser Sign
forall i a. Parser i a -> String -> Parser i a
<?> String
"eq"
{-# INLINE eq #-}

-- | Parse a literal.
--
-- @literal@ supports parsing superfluous parenthesis around arguments
-- of the predicate application, which are not present in the TPTP grammar.
literal :: Parser Literal
literal :: Parser Literal
literal =  Term -> Sign -> Term -> Literal
Equality (Term -> Sign -> Term -> Literal)
-> Parser Term -> Parser Text (Sign -> Term -> Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term -> Parser Term
forall p. Parser p -> Parser p
optionalParens Parser Term
term Parser Text (Sign -> Term -> Literal)
-> Parser Sign -> Parser Text (Term -> Literal)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sign
eq Parser Text (Term -> Literal) -> Parser Term -> Parser Literal
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Term -> Parser Term
forall p. Parser p -> Parser p
optionalParens Parser Term
term
       Parser Literal -> Parser Literal -> Parser Literal
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Name Predicate -> [Term] -> Literal)
-> (Name Predicate, [Term]) -> Literal
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name Predicate -> [Term] -> Literal
Predicate ((Name Predicate, [Term]) -> Literal)
-> Parser Text (Name Predicate, [Term]) -> Parser Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Predicate)
-> Parser Term -> Parser Text (Name Predicate, [Term])
forall f a. Parser f -> Parser a -> Parser (f, [a])
application Parser (Name Predicate)
predicate Parser Term
term
       Parser Literal -> String -> Parser Literal
forall i a. Parser i a -> String -> Parser i a
<?> String
"literal"

-- | Parse a signed literal.
--
-- @signedLiteral@ supports parsing superfluous parenthesis around the literal
-- under the negation sign, which are not present in the TPTP grammar.
signedLiteral :: Parser (Sign, Literal)
signedLiteral :: Parser (Sign, Literal)
signedLiteral =  (Literal -> (Sign, Literal))
-> Parser Literal -> Parser (Sign, Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sign
Negative,) (Char -> Parser Char
op Char
'~' Parser Char -> Parser Literal -> Parser Literal
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Literal -> Parser Literal
forall p. Parser p -> Parser p
optionalParens Parser Literal
literal)
             Parser (Sign, Literal)
-> Parser (Sign, Literal) -> Parser (Sign, Literal)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Literal -> (Sign, Literal))
-> Parser Literal -> Parser (Sign, Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Sign
Positive,) Parser Literal
literal
             Parser (Sign, Literal) -> String -> Parser (Sign, Literal)
forall i a. Parser i a -> String -> Parser i a
<?> String
"signed literal"
{-# INLINE signedLiteral #-}

-- | Parse a clause.
--
-- @clause@ supports parsing superfluous parenthesis around any of the
-- subclauses of the clause, which are not present in the TPTP grammar.
clause :: Parser Clause
clause :: Parser Clause
clause = NonEmpty Clause -> Clause
forall a. Semigroup a => NonEmpty a -> a
sconcat (NonEmpty Clause -> Clause)
-> ([Clause] -> NonEmpty Clause) -> [Clause] -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Clause] -> NonEmpty Clause
forall a. [a] -> NonEmpty a
NEL.fromList ([Clause] -> Clause) -> Parser Text [Clause] -> Parser Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Clause
subclause Parser Clause -> Parser Char -> Parser Text [Clause]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy1` Char -> Parser Char
op Char
'|'
  where
    subclause :: Parser Clause
subclause =  (Sign, Literal) -> Clause
unitClause ((Sign, Literal) -> Clause)
-> Parser (Sign, Literal) -> Parser Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Sign, Literal)
signedLiteral
             Parser Clause -> Parser Clause -> Parser Clause
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Clause -> Parser Clause
forall p. Parser p -> Parser p
parens Parser Clause
clause
             Parser Clause -> String -> Parser Clause
forall i a. Parser i a -> String -> Parser i a
<?> String
"subclause"

-- | Parse a quantifier.
quantifier :: Parser Quantifier
quantifier :: Parser Quantifier
quantifier = Parser Quantifier
forall a. (Named a, Enum a, Bounded a) => Parser a
enum Parser Quantifier -> String -> Parser Quantifier
forall i a. Parser i a -> String -> Parser i a
<?> String
"quantifier"
{-# INLINE quantifier #-}

-- | Parse a logical connective.
connective :: Parser Connective
connective :: Parser Connective
connective = Parser Connective
forall a. (Named a, Enum a, Bounded a) => Parser a
enum Parser Connective -> String -> Parser Connective
forall i a. Parser i a -> String -> Parser i a
<?> String
"connective"
{-# INLINE connective #-}

-- | Given a parser for sort annotations, parse a formula in first-order logic.
firstOrder :: Parser s -> Parser (FirstOrder s)
firstOrder :: Parser s -> Parser (FirstOrder s)
firstOrder Parser s
p = do
  FirstOrder s
f <- Parser (FirstOrder s)
unitary
  FirstOrder s -> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a. Alternative f => a -> f a -> f a
option FirstOrder s
f (FirstOrder s -> Connective -> FirstOrder s -> FirstOrder s
forall s.
FirstOrder s -> Connective -> FirstOrder s -> FirstOrder s
Connected FirstOrder s
f (Connective -> FirstOrder s -> FirstOrder s)
-> Parser Connective -> Parser Text (FirstOrder s -> FirstOrder s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Connective
connective Parser Text (FirstOrder s -> FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser s -> Parser (FirstOrder s)
forall s. Parser s -> Parser (FirstOrder s)
firstOrder Parser s
p)
  where
    unitary :: Parser (FirstOrder s)
unitary =  Literal -> FirstOrder s
forall s. Literal -> FirstOrder s
Atomic     (Literal -> FirstOrder s)
-> Parser Literal -> Parser (FirstOrder s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Literal
literal
           Parser (FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> FirstOrder s -> FirstOrder s
forall s. FirstOrder s -> FirstOrder s
Negated    (FirstOrder s -> FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Parser Char
op Char
'~' Parser Char -> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (FirstOrder s)
unitary)
           Parser (FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Quantifier -> NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s
forall s.
Quantifier -> NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s
Quantified (Quantifier -> NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s)
-> Parser Quantifier
-> Parser Text (NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Quantifier
quantifier Parser Text (NonEmpty (Var, s) -> FirstOrder s -> FirstOrder s)
-> Parser Text (NonEmpty (Var, s))
-> Parser Text (FirstOrder s -> FirstOrder s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text (NonEmpty (Var, s))
vs Parser Text (FirstOrder s -> FirstOrder s)
-> Parser Char -> Parser Text (FirstOrder s -> FirstOrder s)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
':' Parser Text (FirstOrder s -> FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (FirstOrder s)
unitary
           Parser (FirstOrder s)
-> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (FirstOrder s) -> Parser (FirstOrder s)
forall p. Parser p -> Parser p
parens (Parser s -> Parser (FirstOrder s)
forall s. Parser s -> Parser (FirstOrder s)
firstOrder Parser s
p)
           Parser (FirstOrder s) -> String -> Parser (FirstOrder s)
forall i a. Parser i a -> String -> Parser i a
<?> String
"unitary first order"

    vs :: Parser Text (NonEmpty (Var, s))
vs = Parser (Var, s) -> Parser Text (NonEmpty (Var, s))
forall a. Parser a -> Parser (NonEmpty a)
bracketList1 (Parser (Var, s) -> Parser Text (NonEmpty (Var, s)))
-> Parser (Var, s) -> Parser Text (NonEmpty (Var, s))
forall a b. (a -> b) -> a -> b
$ (,) (Var -> s -> (Var, s)) -> Parser Var -> Parser Text (s -> (Var, s))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
var Parser Text (s -> (Var, s)) -> Parser s -> Parser (Var, s)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser s
p

-- | Parse a formula in unsorted first-order logic.
unsortedFirstOrder :: Parser UnsortedFirstOrder
unsortedFirstOrder :: Parser UnsortedFirstOrder
unsortedFirstOrder = Parser Unsorted -> Parser UnsortedFirstOrder
forall s. Parser s -> Parser (FirstOrder s)
firstOrder Parser Unsorted
forall i. Parser i Unsorted
unsorted
  where unsorted :: Parser i Unsorted
unsorted = Unsorted -> Parser i Unsorted
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Unsorted
Unsorted ()) Parser i Unsorted -> String -> Parser i Unsorted
forall i a. Parser i a -> String -> Parser i a
<?> String
"unsorted"

sorted :: Parser s -> Parser (Sorted s)
sorted :: Parser s -> Parser (Sorted s)
sorted Parser s
s = Maybe s -> Sorted s
forall s. Maybe s -> Sorted s
Sorted (Maybe s -> Sorted s) -> Parser Text (Maybe s) -> Parser (Sorted s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser s -> Parser Text (Maybe s)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Char -> Parser Char
op Char
':' Parser Char -> Parser s -> Parser s
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser s -> Parser s
forall p. Parser p -> Parser p
optionalParens Parser s
s) Parser (Sorted s) -> String -> Parser (Sorted s)
forall i a. Parser i a -> String -> Parser i a
<?> String
"sorted"

-- | An alias for 'monomorphicFirstOrder'.
sortedFirstOrder :: Parser SortedFirstOrder
sortedFirstOrder :: Parser SortedFirstOrder
sortedFirstOrder = Parser SortedFirstOrder
monomorphicFirstOrder

-- | Parse a formula in sorted monomorphic first-order logic.
monomorphicFirstOrder :: Parser MonomorphicFirstOrder
monomorphicFirstOrder :: Parser SortedFirstOrder
monomorphicFirstOrder = Parser (Sorted (Name Sort)) -> Parser SortedFirstOrder
forall s. Parser s -> Parser (FirstOrder s)
firstOrder (Parser (Name Sort) -> Parser (Sorted (Name Sort))
forall s. Parser s -> Parser (Sorted s)
sorted Parser (Name Sort)
sort) Parser SortedFirstOrder -> String -> Parser SortedFirstOrder
forall i a. Parser i a -> String -> Parser i a
<?> String
"tff0"

quantifiedSort :: Parser QuantifiedSort
quantifiedSort :: Parser QuantifiedSort
quantifiedSort = Text -> Parser Text
token Text
"$tType" Parser Text -> QuantifiedSort -> Parser QuantifiedSort
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> () -> QuantifiedSort
QuantifiedSort ()

-- | Parse a formula in sorted polymorphic first-order logic.
polymorphicFirstOrder :: Parser PolymorphicFirstOrder
polymorphicFirstOrder :: Parser PolymorphicFirstOrder
polymorphicFirstOrder =  Parser (Sorted (Either QuantifiedSort TFF1Sort))
-> Parser PolymorphicFirstOrder
forall s. Parser s -> Parser (FirstOrder s)
firstOrder (Parser (Either QuantifiedSort TFF1Sort)
-> Parser (Sorted (Either QuantifiedSort TFF1Sort))
forall s. Parser s -> Parser (Sorted s)
sorted (Parser QuantifiedSort
-> Parser TFF1Sort -> Parser (Either QuantifiedSort TFF1Sort)
forall (f :: * -> *) a b.
Alternative f =>
f a -> f b -> f (Either a b)
eitherP Parser QuantifiedSort
quantifiedSort Parser TFF1Sort
tff1Sort))
                     Parser PolymorphicFirstOrder
-> String -> Parser PolymorphicFirstOrder
forall i a. Parser i a -> String -> Parser i a
<?> String
"tff1"


-- ** Units

-- | Parse a formula in a given TPTP language.
formula :: Language -> Parser Formula
formula :: Language -> Parser Formula
formula = \case
  Language
CNF_ -> Clause -> Formula
CNF (Clause -> Formula) -> Parser Clause -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Clause
clause Parser Formula -> String -> Parser Formula
forall i a. Parser i a -> String -> Parser i a
<?> String
"cnf"
  Language
FOF_ -> UnsortedFirstOrder -> Formula
FOF (UnsortedFirstOrder -> Formula)
-> Parser UnsortedFirstOrder -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser UnsortedFirstOrder
unsortedFirstOrder Parser Formula -> String -> Parser Formula
forall i a. Parser i a -> String -> Parser i a
<?> String
"fof"
  Language
TFF_ -> PolymorphicFirstOrder -> Formula
tff (PolymorphicFirstOrder -> Formula)
-> Parser PolymorphicFirstOrder -> Parser Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser PolymorphicFirstOrder
polymorphicFirstOrder Parser Formula -> String -> Parser Formula
forall i a. Parser i a -> String -> Parser i a
<?> String
"tff"
  where
    tff :: PolymorphicFirstOrder -> Formula
tff PolymorphicFirstOrder
f = case PolymorphicFirstOrder -> Maybe SortedFirstOrder
monomorphizeFirstOrder PolymorphicFirstOrder
f of
     Just SortedFirstOrder
f' -> SortedFirstOrder -> Formula
TFF0 SortedFirstOrder
f'
     Maybe SortedFirstOrder
Nothing -> PolymorphicFirstOrder -> Formula
TFF1 PolymorphicFirstOrder
f

-- | Parse a formula role.
role :: Parser (Reserved Role)
role :: Parser (Reserved Role)
role = Parser (Reserved Role)
forall a. (Named a, Enum a, Bounded a) => Parser (Reserved a)
reserved Parser (Reserved Role) -> String -> Parser (Reserved Role)
forall i a. Parser i a -> String -> Parser i a
<?> String
"role"
{-# INLINE role #-}

-- | Parse the name of a TPTP language.
language :: Parser Language
language :: Parser Language
language = Parser Language
forall a. (Named a, Enum a, Bounded a) => Parser a
enum Parser Language -> String -> Parser Language
forall i a. Parser i a -> String -> Parser i a
<?> String
"language"
{-# INLINE language #-}

-- | Parse a TPTP declaration in a given language.
declaration :: Language -> Parser Declaration
declaration :: Language -> Parser Declaration
declaration Language
l =  Text -> Parser Text
token Text
"type" Parser Text -> Parser Declaration -> Parser Declaration
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Declaration -> Parser Declaration
forall p. Parser p -> Parser p
comma (Parser Declaration -> Parser Declaration
forall p. Parser p -> Parser p
optionalParens Parser Declaration
typeDeclaration)
             Parser Declaration -> Parser Declaration -> Parser Declaration
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Reserved Role -> Formula -> Declaration
Formula (Reserved Role -> Formula -> Declaration)
-> Parser (Reserved Role) -> Parser Text (Formula -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Reserved Role)
role Parser Text (Formula -> Declaration)
-> Parser Formula -> Parser Declaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Formula -> Parser Formula
forall p. Parser p -> Parser p
comma (Language -> Parser Formula
formula Language
l)
             Parser Declaration -> String -> Parser Declaration
forall i a. Parser i a -> String -> Parser i a
<?> String
"declaration"

-- | Parse a declaration with the @type@ role - either a typing relation or
-- a sort declaration.
typeDeclaration :: Parser Declaration
typeDeclaration :: Parser Declaration
typeDeclaration =  Atom -> Integer -> Declaration
Sort   (Atom -> Integer -> Declaration)
-> Parser Atom -> Parser Text (Integer -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom Parser Text (Integer -> Declaration)
-> Parser Char -> Parser Text (Integer -> Declaration)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
':' Parser Text (Integer -> Declaration)
-> Parser Integer -> Parser Declaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer -> Parser Integer
forall p. Parser p -> Parser p
optionalParens Parser Integer
arity
               Parser Declaration -> Parser Declaration -> Parser Declaration
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Atom -> Type -> Declaration
Typing (Atom -> Type -> Declaration)
-> Parser Atom -> Parser Text (Type -> Declaration)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom Parser Text (Type -> Declaration)
-> Parser Char -> Parser Text (Type -> Declaration)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
':' Parser Text (Type -> Declaration)
-> Parser Type -> Parser Declaration
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Type -> Parser Type
forall p. Parser p -> Parser p
optionalParens Parser Type
type_
               Parser Declaration -> String -> Parser Declaration
forall i a. Parser i a -> String -> Parser i a
<?> String
"type declaration"
  where
    arity :: Parser Integer
arity = [Text] -> Integer
forall i a. Num i => [a] -> i
genericLength ([Text] -> Integer)
-> (([Text], Text) -> [Text]) -> ([Text], Text) -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Text], Text) -> [Text]
forall a b. (a, b) -> a
fst (([Text], Text) -> Integer)
-> Parser Text ([Text], Text) -> Parser Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text -> Parser Text ([Text], Text)
forall a. Parser a -> Parser ([a], a)
mapping (Parser Text -> Parser Text
forall p. Parser p -> Parser p
optionalParens (Text -> Parser Text
token Text
"$tType"))

-- | Parse a unit name.
unitName :: Parser (Either Atom Integer)
unitName :: Parser (Either Atom Integer)
unitName = Parser Atom -> Parser Integer -> Parser (Either Atom Integer)
forall (f :: * -> *) a b.
Alternative f =>
f a -> f b -> f (Either a b)
eitherP Parser Atom
atom (Parser Integer -> Parser Integer
forall a. Num a => Parser a -> Parser a
signed Parser Integer
integer) Parser (Either Atom Integer)
-> String -> Parser (Either Atom Integer)
forall i a. Parser i a -> String -> Parser i a
<?> String
"unit name"
{-# INLINE unitName #-}

-- | Parse a list of unit names.
unitNames :: Parser (NonEmpty UnitName)
unitNames :: Parser (NonEmpty (Either Atom Integer))
unitNames = Parser (Either Atom Integer)
-> Parser (NonEmpty (Either Atom Integer))
forall a. Parser a -> Parser (NonEmpty a)
bracketList1 Parser (Either Atom Integer)
unitName Parser (NonEmpty (Either Atom Integer))
-> String -> Parser (NonEmpty (Either Atom Integer))
forall i a. Parser i a -> String -> Parser i a
<?> String
"unit names"
{-# INLINE unitNames #-}

-- | Parse an @include@ statement.
include :: Parser Unit
include :: Parser Unit
include =  Text -> Parser Unit -> Parser Unit
forall a. Text -> Parser a -> Parser a
labeled Text
"include" (Atom -> Maybe (NonEmpty (Either Atom Integer)) -> Unit
Include (Atom -> Maybe (NonEmpty (Either Atom Integer)) -> Unit)
-> Parser Atom
-> Parser Text (Maybe (NonEmpty (Either Atom Integer)) -> Unit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom Parser Text (Maybe (NonEmpty (Either Atom Integer)) -> Unit)
-> Parser Text (Maybe (NonEmpty (Either Atom Integer)))
-> Parser Unit
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (NonEmpty (Either Atom Integer))
-> Parser Text (Maybe (NonEmpty (Either Atom Integer)))
forall a. Parser a -> Parser (Maybe a)
maybeP Parser (NonEmpty (Either Atom Integer))
unitNames) Parser Unit -> Parser Char -> Parser Unit
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
'.'
       Parser Unit -> String -> Parser Unit
forall i a. Parser i a -> String -> Parser i a
<?> String
"include"

-- | Parse an annotated unit.
annotatedUnit :: Parser Unit
annotatedUnit :: Parser Unit
annotatedUnit = do
  Language
l <- Parser Language
language
  let n :: Parser (Either Atom Integer)
n = Parser (Either Atom Integer)
unitName
  let d :: Parser Declaration
d = Language -> Parser Declaration
declaration Language
l
  let a :: Parser (Maybe Annotation)
a = Parser Annotation -> Parser (Maybe Annotation)
forall a. Parser a -> Parser (Maybe a)
maybeP Parser Annotation
annotation
  Parser Unit -> Parser Unit
forall p. Parser p -> Parser p
parens (Either Atom Integer -> Declaration -> Maybe Annotation -> Unit
Unit (Either Atom Integer -> Declaration -> Maybe Annotation -> Unit)
-> Parser (Either Atom Integer)
-> Parser Text (Declaration -> Maybe Annotation -> Unit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Either Atom Integer)
n Parser Text (Declaration -> Maybe Annotation -> Unit)
-> Parser Declaration -> Parser Text (Maybe Annotation -> Unit)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Declaration -> Parser Declaration
forall p. Parser p -> Parser p
comma Parser Declaration
d Parser Text (Maybe Annotation -> Unit)
-> Parser (Maybe Annotation) -> Parser Unit
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe Annotation)
a) Parser Unit -> Parser Char -> Parser Unit
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Char -> Parser Char
op Char
'.'
  Parser Unit -> String -> Parser Unit
forall i a. Parser i a -> String -> Parser i a
<?> String
"annotated unit"

-- | Parse a TPTP unit.
unit :: Parser Unit
unit :: Parser Unit
unit = Parser Unit
include Parser Unit -> Parser Unit -> Parser Unit
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Unit
annotatedUnit Parser Unit -> String -> Parser Unit
forall i a. Parser i a -> String -> Parser i a
<?> String
"unit"

-- | Parse a TPTP input.
tptp :: Parser TPTP
tptp :: Parser TPTP
tptp = [Unit] -> TPTP
TPTP ([Unit] -> TPTP) -> Parser Text [Unit] -> Parser TPTP
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Unit -> Parser () -> Parser Text [Unit]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
manyTill Parser Unit
unit Parser ()
forall t. Chunk t => Parser t ()
endOfInput Parser TPTP -> String -> Parser TPTP
forall i a. Parser i a -> String -> Parser i a
<?> String
"tptp"

-- | Parse a TSTP input.
tstp :: Parser TSTP
tstp :: Parser TSTP
tstp =  Parser ()
skipSpace Parser () -> Parser TSTP -> Parser TSTP
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (SZS -> [Unit] -> TSTP
TSTP (SZS -> [Unit] -> TSTP)
-> Parser Text SZS -> Parser Text ([Unit] -> TSTP)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text SZS
szs Parser Text ([Unit] -> TSTP) -> Parser Text [Unit] -> Parser TSTP
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Unit -> Parser () -> Parser Text [Unit]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
manyTill Parser Unit
unit Parser ()
forall t. Chunk t => Parser t ()
endOfInput) Parser TSTP -> Parser () -> Parser TSTP
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall t. Chunk t => Parser t ()
endOfInput
    Parser TSTP -> String -> Parser TSTP
forall i a. Parser i a -> String -> Parser i a
<?> String
"tstp"


-- ** Annotations

instance Semigroup SZS where
  SZS Maybe Status
s Maybe Dataform
d <> :: SZS -> SZS -> SZS
<> SZS Maybe Status
s' Maybe Dataform
d' = Maybe Status -> Maybe Dataform -> SZS
SZS (Maybe Status
s Maybe Status -> Maybe Status -> Maybe Status
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Status
s') (Maybe Dataform
d Maybe Dataform -> Maybe Dataform -> Maybe Dataform
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe Dataform
d')

instance Monoid SZS where
  mempty :: SZS
mempty = Maybe Status -> Maybe Dataform -> SZS
SZS Maybe Status
forall (f :: * -> *) a. Alternative f => f a
empty Maybe Dataform
forall (f :: * -> *) a. Alternative f => f a
empty
  mappend :: SZS -> SZS -> SZS
mappend = SZS -> SZS -> SZS
forall a. Semigroup a => a -> a -> a
(<>)

-- | Parse the SZS ontology information of a TSTP output inside a comment.
szs :: Parser SZS
szs :: Parser Text SZS
szs = SZS -> Maybe SZS -> SZS
forall a. a -> Maybe a -> a
fromMaybe SZS
forall a. Monoid a => a
mempty (Maybe SZS -> SZS)
-> ([Maybe SZS] -> Maybe SZS) -> [Maybe SZS] -> SZS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe SZS] -> Maybe SZS
forall a. Monoid a => [a] -> a
mconcat ([Maybe SZS] -> SZS) -> Parser Text [Maybe SZS] -> Parser Text SZS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (Maybe SZS) -> Parser Text [Maybe SZS]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser Text (Maybe SZS)
szsComment

szsComment :: Parser (Maybe SZS)
szsComment :: Parser Text (Maybe SZS)
szsComment =  Parser Text (Maybe SZS) -> Parser Text (Maybe SZS)
forall p. Parser p -> Parser p
commented (Parser ()
skipSpace Parser () -> Parser Text (Maybe ()) -> Parser Text (Maybe ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
                         Parser () -> Parser Text (Maybe ())
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser ()
skipBeginComment Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace) Parser Text (Maybe ())
-> Parser Text (Maybe SZS) -> Parser Text (Maybe SZS)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
                         Parser Text SZS -> Parser Text (Maybe SZS)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser Text SZS
szsAnnotation)
          Parser Text (Maybe SZS) -> Parser () -> Parser Text (Maybe SZS)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*  Parser ()
skipSpace
          Parser Text (Maybe SZS) -> String -> Parser Text (Maybe SZS)
forall i a. Parser i a -> String -> Parser i a
<?> String
"szs comment"

szsAnnotation :: Parser SZS
szsAnnotation :: Parser Text SZS
szsAnnotation =  Text -> Parser Text
string Text
"SZS" Parser Text -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace Parser () -> Parser Text SZS -> Parser Text SZS
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Parser Text SZS
szsStatus Parser Text SZS -> Parser Text SZS -> Parser Text SZS
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Text SZS
szsDataform)
             Parser Text SZS -> String -> Parser Text SZS
forall i a. Parser i a -> String -> Parser i a
<?> String
"szs annotation"

szsStatus :: Parser SZS
szsStatus :: Parser Text SZS
szsStatus =  Text -> Parser Text
string Text
"status" Parser Text -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace
          Parser () -> Parser Text SZS -> Parser Text SZS
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Status -> SZS
fromStatus (Status -> SZS) -> Parser Text Status -> Parser Text SZS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Status
status)
         Parser Text SZS -> String -> Parser Text SZS
forall i a. Parser i a -> String -> Parser i a
<?> String
"status"
  where
    fromStatus :: Status -> SZS
fromStatus Status
s = Maybe Status -> Maybe Dataform -> SZS
SZS (Status -> Maybe Status
forall a. a -> Maybe a
Just Status
s) Maybe Dataform
forall a. Maybe a
Nothing
    status :: Parser Text Status
status = Parser Text NoSuccess -> Parser Text Success -> Parser Text Status
forall (f :: * -> *) a b.
Alternative f =>
f a -> f b -> f (Either a b)
eitherP (SZSOntology NoSuccess -> NoSuccess
forall a. SZSOntology a -> a
unwrapSZSOntology (SZSOntology NoSuccess -> NoSuccess)
-> Parser Text (SZSOntology NoSuccess) -> Parser Text NoSuccess
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (SZSOntology NoSuccess)
forall a. (Named a, Enum a, Bounded a) => Parser a
named)
                     (SZSOntology Success -> Success
forall a. SZSOntology a -> a
unwrapSZSOntology (SZSOntology Success -> Success)
-> Parser Text (SZSOntology Success) -> Parser Text Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (SZSOntology Success)
forall a. (Named a, Enum a, Bounded a) => Parser a
named)

szsDataform :: Parser SZS
szsDataform :: Parser Text SZS
szsDataform =  Text -> Parser Text
string Text
"output" Parser Text -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace
            Parser () -> Parser Text -> Parser Text
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Text -> Parser Text
string Text
"start"  Parser Text -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
skipSpace
            Parser () -> Parser Text SZS -> Parser Text SZS
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Dataform -> SZS
fromDataform (Dataform -> SZS) -> Parser Text Dataform -> Parser Text SZS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Dataform
dataform)
           Parser Text SZS -> String -> Parser Text SZS
forall i a. Parser i a -> String -> Parser i a
<?> String
"dataform"
  where
    fromDataform :: Dataform -> SZS
fromDataform Dataform
d = Maybe Status -> Maybe Dataform -> SZS
SZS Maybe Status
forall a. Maybe a
Nothing (Dataform -> Maybe Dataform
forall a. a -> Maybe a
Just Dataform
d)
    dataform :: Parser Text Dataform
dataform = SZSOntology Dataform -> Dataform
forall a. SZSOntology a -> a
unwrapSZSOntology (SZSOntology Dataform -> Dataform)
-> Parser Text (SZSOntology Dataform) -> Parser Text Dataform
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (SZSOntology Dataform)
forall a. (Named a, Enum a, Bounded a) => Parser a
named

-- | Parse an introduction marking.
intro :: Parser Intro
intro :: Parser Intro
intro = Parser Intro
forall a. (Named a, Enum a, Bounded a) => Parser a
enum Parser Intro -> String -> Parser Intro
forall i a. Parser i a -> String -> Parser i a
<?> String
"intro"
{-# INLINE intro #-}

-- | Parse a unit of information about a formula.
info :: Parser Info
info :: Parser Info
info =  Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"description" (Atom -> Info
Description (Atom -> Info) -> Parser Atom -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"iquote"      (Atom -> Info
Iquote      (Atom -> Info) -> Parser Atom -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"status"      (Reserved Success -> Info
Status      (Reserved Success -> Info)
-> Parser Text (Reserved Success) -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (Reserved Success)
forall a. (Named a, Enum a, Bounded a) => Parser (Reserved a)
reserved)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"assumptions" (NonEmpty (Either Atom Integer) -> Info
Assumptions (NonEmpty (Either Atom Integer) -> Info)
-> Parser (NonEmpty (Either Atom Integer)) -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (NonEmpty (Either Atom Integer))
unitNames)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"refutation"  (Atom -> Info
Refutation  (Atom -> Info) -> Parser Atom -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"new_symbols" (Atom -> [Either Var Atom] -> Info
NewSymbols  (Atom -> [Either Var Atom] -> Info)
-> Parser Atom -> Parser Text ([Either Var Atom] -> Info)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom Parser Text ([Either Var Atom] -> Info)
-> Parser Text [Either Var Atom] -> Parser Info
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Either Var Atom] -> Parser Text [Either Var Atom]
forall p. Parser p -> Parser p
comma Parser Text [Either Var Atom]
symbols)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Info -> Parser Info
forall a. Text -> Parser a -> Parser a
labeled Text
"bind"        (Var -> Expression -> Info
Bind (Var -> Expression -> Info)
-> Parser Var -> Parser Text (Expression -> Info)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Var
var Parser Text (Expression -> Info)
-> Parser Text Expression -> Parser Info
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text Expression -> Parser Text Expression
forall p. Parser p -> Parser p
comma Parser Text Expression
expr)
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expression -> Info
Expression (Expression -> Info) -> Parser Text Expression -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Expression
expr
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Atom -> [Info] -> Info) -> (Atom, [Info]) -> Info
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Atom -> [Info] -> Info
Application ((Atom, [Info]) -> Info)
-> Parser Text (Atom, [Info]) -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom -> Parser Info -> Parser Text (Atom, [Info])
forall f a. Parser f -> Parser a -> Parser (f, [a])
application Parser Atom
atom Parser Info
info
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Number -> Info
InfoNumber (Number -> Info) -> Parser Number -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Number
number
    Parser Info -> Parser Info -> Parser Info
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Info] -> Info
Infos ([Info] -> Info) -> Parser Text [Info] -> Parser Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text [Info]
infos
  where
    symbols :: Parser Text [Either Var Atom]
symbols = Parser (Either Var Atom) -> Parser Text [Either Var Atom]
forall a. Parser a -> Parser [a]
bracketList (Parser Var -> Parser Atom -> Parser (Either Var Atom)
forall (f :: * -> *) a b.
Alternative f =>
f a -> f b -> f (Either a b)
eitherP Parser Var
var Parser Atom
atom)

infos :: Parser [Info]
infos :: Parser Text [Info]
infos = Parser Info -> Parser Text [Info]
forall a. Parser a -> Parser [a]
bracketList Parser Info
info Parser Text [Info] -> String -> Parser Text [Info]
forall i a. Parser i a -> String -> Parser i a
<?> String
"infos"
{-# INLINE infos #-}

-- | Parse an expression.
expr :: Parser Expression
expr :: Parser Text Expression
expr =  Char -> Parser Char
char Char
'$' Parser Char -> Parser Text Expression -> Parser Text Expression
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Text -> Parser Text Expression -> Parser Text Expression
forall a. Text -> Parser a -> Parser a
labeled Text
"fot" (Term -> Expression
Term (Term -> Expression) -> Parser Term -> Parser Text Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term -> Parser Term
forall p. Parser p -> Parser p
optionalParens Parser Term
term)
                Parser Text Expression
-> Parser Text Expression -> Parser Text Expression
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>  Formula -> Expression
Logical (Formula -> Expression) -> Parser Formula -> Parser Text Expression
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Language
language Parser Language -> (Language -> Parser Formula) -> Parser Formula
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Parser Formula -> Parser Formula
forall p. Parser p -> Parser p
parens (Parser Formula -> Parser Formula)
-> (Language -> Parser Formula) -> Language -> Parser Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Formula -> Parser Formula
forall p. Parser p -> Parser p
optionalParens (Parser Formula -> Parser Formula)
-> (Language -> Parser Formula) -> Language -> Parser Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Language -> Parser Formula
formula))
    Parser Text Expression -> String -> Parser Text Expression
forall i a. Parser i a -> String -> Parser i a
<?> String
"expression"

-- | Parse a parent.
parent :: Parser Parent
parent :: Parser Parent
parent = Source -> [Info] -> Parent
Parent (Source -> [Info] -> Parent)
-> Parser Text Source -> Parser Text ([Info] -> Parent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Source
source Parser Text ([Info] -> Parent)
-> Parser Text [Info] -> Parser Parent
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Info] -> Parser Text [Info] -> Parser Text [Info]
forall (f :: * -> *) a. Alternative f => a -> f a -> f a
option [] (Char -> Parser Char
op Char
':' Parser Char -> Parser Text [Info] -> Parser Text [Info]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Text [Info]
infos) Parser Parent -> String -> Parser Parent
forall i a. Parser i a -> String -> Parser i a
<?> String
"parent"

-- | Parse the source of a unit.
source :: Parser Source
source :: Parser Text Source
source =  Text -> Parser Text
token Text
"unknown" Parser Text -> Source -> Parser Text Source
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Source
UnknownSource
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Source -> Parser Text Source
forall a. Text -> Parser a -> Parser a
labeled Text
"file"       (Atom -> Maybe (Either Atom Integer) -> Source
File       (Atom -> Maybe (Either Atom Integer) -> Source)
-> Parser Atom
-> Parser Text (Maybe (Either Atom Integer) -> Source)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom     Parser Text (Maybe (Either Atom Integer) -> Source)
-> Parser Text (Maybe (Either Atom Integer)) -> Parser Text Source
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Either Atom Integer)
-> Parser Text (Maybe (Either Atom Integer))
forall a. Parser a -> Parser (Maybe a)
maybeP Parser (Either Atom Integer)
unitName)
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Source -> Parser Text Source
forall a. Text -> Parser a -> Parser a
labeled Text
"theory"     (Atom -> Maybe [Info] -> Source
Theory     (Atom -> Maybe [Info] -> Source)
-> Parser Atom -> Parser Text (Maybe [Info] -> Source)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom     Parser Text (Maybe [Info] -> Source)
-> Parser Text (Maybe [Info]) -> Parser Text Source
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Info] -> Parser Text (Maybe [Info])
forall a. Parser a -> Parser (Maybe a)
maybeP Parser Text [Info]
infos)
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Source -> Parser Text Source
forall a. Text -> Parser a -> Parser a
labeled Text
"creator"    (Atom -> Maybe [Info] -> Source
Creator    (Atom -> Maybe [Info] -> Source)
-> Parser Atom -> Parser Text (Maybe [Info] -> Source)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom     Parser Text (Maybe [Info] -> Source)
-> Parser Text (Maybe [Info]) -> Parser Text Source
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Info] -> Parser Text (Maybe [Info])
forall a. Parser a -> Parser (Maybe a)
maybeP Parser Text [Info]
infos)
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Source -> Parser Text Source
forall a. Text -> Parser a -> Parser a
labeled Text
"introduced" (Reserved Intro -> Maybe [Info] -> Source
Introduced (Reserved Intro -> Maybe [Info] -> Source)
-> Parser Text (Reserved Intro)
-> Parser Text (Maybe [Info] -> Source)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text (Reserved Intro)
forall a. (Named a, Enum a, Bounded a) => Parser (Reserved a)
reserved Parser Text (Maybe [Info] -> Source)
-> Parser Text (Maybe [Info]) -> Parser Text Source
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Info] -> Parser Text (Maybe [Info])
forall a. Parser a -> Parser (Maybe a)
maybeP Parser Text [Info]
infos)
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Text -> Parser Text Source -> Parser Text Source
forall a. Text -> Parser a -> Parser a
labeled Text
"inference"  (Atom -> [Info] -> [Parent] -> Source
Inference  (Atom -> [Info] -> [Parent] -> Source)
-> Parser Atom -> Parser Text ([Info] -> [Parent] -> Source)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Atom
atom     Parser Text ([Info] -> [Parent] -> Source)
-> Parser Text [Info] -> Parser Text ([Parent] -> Source)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Info] -> Parser Text [Info]
forall p. Parser p -> Parser p
comma  Parser Text [Info]
infos
                                           Parser Text ([Parent] -> Source)
-> Parser Text [Parent] -> Parser Text Source
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Parent] -> Parser Text [Parent]
forall p. Parser p -> Parser p
comma (Parser Parent -> Parser Text [Parent]
forall a. Parser a -> Parser [a]
bracketList Parser Parent
parent))
      Parser Text Source -> Parser Text Source -> Parser Text Source
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Either Atom Integer -> Source
UnitSource (Either Atom Integer -> Source)
-> Parser (Either Atom Integer) -> Parser Text Source
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Either Atom Integer)
unitName
      Parser Text Source -> String -> Parser Text Source
forall i a. Parser i a -> String -> Parser i a
<?> String
"source"

-- | Parse an annotation.
annotation :: Parser Annotation
annotation :: Parser Annotation
annotation = (,) (Source -> Maybe [Info] -> Annotation)
-> Parser Text Source -> Parser Text (Maybe [Info] -> Annotation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Text Source
source Parser Text (Maybe [Info] -> Annotation)
-> Parser Text (Maybe [Info]) -> Parser Annotation
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Text [Info] -> Parser Text (Maybe [Info])
forall a. Parser a -> Parser (Maybe a)
maybeP Parser Text [Info]
infos Parser Annotation -> String -> Parser Annotation
forall i a. Parser i a -> String -> Parser i a
<?> String
"annotation"