-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Import, export etc. for TPTP, a syntax for first-order logic
--   
--   For information about the TPTP format, see
--   <a>http://www.cs.miami.edu/~tptp/</a>.
--   
--   Components:
--   
--   <ul>
--   <li>Parser (<a>parse</a>)</li>
--   <li>Exporter (<a>toTPTP</a>)</li>
--   <li>Pretty-printer (<a>pretty</a>)</li>
--   <li>QuickCheck instances (generation of random formulae)</li>
--   <li><a>diff</a> : Get a "formula" which represents the differences
--   between two given formulae (equal subexpressions are truncated; so are
--   the subexpressions of subexpressions whose heads already differ)</li>
--   </ul>
--   
--   Tests passed:
--   
--   <ul>
--   <li>For randomly generated formulae, <tt>parse . toTPTP ==
--   id</tt></li>
--   <li>For all files in the TPTP (v 5.2.0) distribution's
--   <tt>Problems</tt> subtree which don't match the regex "^(thf|tff)(",
--   <tt>parse . toTPTP . parse == parse</tt></li>
--   </ul>
--   
--   Not yet implemented: The new <i>thf</i> and <i>tff</i> formula types.
@package logic-TPTP
@version 0.3.0.2

module Codec.TPTP.Base

-- | Basic (undecorated) first-order formulae
type Formula = F Identity

-- | Basic (undecorated) terms
type Term = T Identity

-- | First-order formulae decorated with state
type FormulaST s = F (State s)

-- | Terms decorated with state
type TermST s = T (State s)

-- | First-order formulae decorated with comments
type FormulaC = FormulaST [String]

-- | Terms decorated with comments
type TermC = TermST [String]

-- | Forget comments in formulae decoreated with comments
forgetFC :: FormulaC -> Formula

-- | Forget comments in terms decoreated with comments
forgetTC :: TermC -> Term

-- | Equivalence
--   
--   Don't let the type context of these wrapper function confuse you :) --
--   the important special case is just:
--   
--   <pre>
--   (.&lt;=&gt;.) :: <a>Formula</a> -&gt; <a>Formula</a> -&gt; <a>Formula</a>
--   </pre>
(.<=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | Implication
(.=>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | Reverse implication
(.<=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | Disjunction/OR
(.|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | Conjunction/AND
(.&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | XOR
(.<~>.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | NOR
(.~|.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | NAND
(.~&.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> (F c) -> F c

-- | Negation
(.~.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (F c) -> F c

-- | Equality
(.=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (T c) -> (T c) -> F c

-- | Inequality
(.!=.) :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => (T c) -> (T c) -> F c

-- | Universal quantification
for_all :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> (F c) -> F c

-- | Existential quantification
exists :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => [V] -> (F c) -> F c

-- | Predicate symbol application
pApp :: Pointed (Formula0 (T c) (F c)) (c (Formula0 (T c) (F c))) => AtomicWord -> [T c] -> F c

-- | Variable
var :: Pointed (Term0 (T c)) (c (Term0 (T c))) => V -> T c

-- | Function symbol application (constants are encoded as nullary
--   functions)
fApp :: Pointed (Term0 (T c)) (c (Term0 (T c))) => AtomicWord -> [T c] -> T c

-- | Number literal
numberLitTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => Rational -> T c

-- | Double-quoted string literal, called <i>Distinct Object</i> in TPTP's
--   grammar
distinctObjectTerm :: Pointed (Term0 (T c)) (c (Term0 (T c))) => String -> T c

-- | See <a>http://haskell.org/haskellwiki/Indirect_composite</a> for the
--   point of the type parameters (they allow for future decorations, e.g.
--   monadic subformulae). If you don't need decorations, you can just use
--   <a>Formula</a> and the wrapped constructors above.
data Formula0 term formula

-- | Binary connective application
BinOp :: formula -> BinOp -> formula -> Formula0 term formula

-- | Infix predicate application (equalities, inequalities)
InfixPred :: term -> InfixPred -> term -> Formula0 term formula

-- | Predicate application
PredApp :: AtomicWord -> [term] -> Formula0 term formula

-- | Quantified formula
Quant :: Quant -> [V] -> formula -> Formula0 term formula

-- | Negation
(:~:) :: formula -> Formula0 term formula

-- | See <a>http://haskell.org/haskellwiki/Indirect_composite</a> for the
--   point of the type parameters (they allow for future decorations). If
--   you don't need decorations, you can just use <a>Term</a> and the
--   wrapped constructors above.
data Term0 term

-- | Variable
Var :: V -> Term0 term

-- | Number literal
NumberLitTerm :: Rational -> Term0 term

-- | Double-quoted item
DistinctObjectTerm :: String -> Term0 term

-- | Function symbol application (constants are encoded as nullary
--   functions)
FunApp :: AtomicWord -> [term] -> Term0 term

-- | Formulae whose subexpressions are wrapped in the given type
--   constructor <tt>c</tt>.
--   
--   For example:
--   
--   <ul>
--   <li><tt>c = <a>Identity</a></tt>: Plain formulae</li>
--   <li><tt>c = <a>Maybe</a></tt>: Formulae that may contain "holes"</li>
--   <li><tt>c = <tt>IORef</tt></tt>: (Mutable) formulae with mutable
--   subexpressions</li>
--   </ul>
newtype F c
F :: c (Formula0 (T c) (F c)) -> F c
runF :: F c -> c (Formula0 (T c) (F c))

-- | Terms whose subterms are wrapped in the given type constructor
--   <tt>c</tt>
newtype T c
T :: c (Term0 (T c)) -> T c
runT :: T c -> c (Term0 (T c))

-- | Binary formula connectives
data BinOp

-- | Equivalence
(:<=>:) :: BinOp

-- | Implication
(:=>:) :: BinOp

-- | Reverse Implication
(:<=:) :: BinOp

-- | AND
(:&:) :: BinOp

-- | OR
(:|:) :: BinOp

-- | NAND
(:~&:) :: BinOp

-- | NOR
(:~|:) :: BinOp

-- | XOR
(:<~>:) :: BinOp

-- | <i>Term -&gt; Term -&gt; Formula</i> infix connectives
data InfixPred
(:=:) :: InfixPred
(:!=:) :: InfixPred

-- | Quantifier specification
data Quant
All :: Quant
Exists :: Quant

-- | A line of a TPTP file: Annotated formula, comment or include
--   statement.
type TPTP_Input = TPTP_Input_ Identity

-- | A line of a TPTP file: Annotated formula (with the comment string
--   embbeded in the State monad ), comment or include statement
type TPTP_Input_C = TPTP_Input_ (State [String])

-- | Forget comments in a line of a TPTP file decoreated with comments
forgetTIC :: TPTP_Input_C -> TPTP_Input

-- | Generalized TPTP_Input
data TPTP_Input_ c

-- | Annotated formulae
AFormula :: AtomicWord -> Role -> F c -> Annotations -> TPTP_Input_ c
name :: TPTP_Input_ c -> AtomicWord
role :: TPTP_Input_ c -> Role
formula :: TPTP_Input_ c -> F c
annotations :: TPTP_Input_ c -> Annotations
Comment :: String -> TPTP_Input_ c
Include :: FilePath -> [AtomicWord] -> TPTP_Input_ c

-- | Annotations about the formulas origin
data Annotations
NoAnnotations :: Annotations
Annotations :: GTerm -> UsefulInfo -> Annotations

-- | Misc annotations
data UsefulInfo
NoUsefulInfo :: UsefulInfo
UsefulInfo :: [GTerm] -> UsefulInfo

-- | Formula roles -- why isn't this newtype??
data Role
Role :: String -> Role
unrole :: Role -> String

-- | Metadata (the <i>general_data</i> rule in TPTP's grammar)
data GData
GWord :: AtomicWord -> GData
GApp :: AtomicWord -> [GTerm] -> GData
GVar :: V -> GData
GNumber :: Rational -> GData
GDistinctObject :: String -> GData
GFormulaData :: String -> Formula -> GData

-- | Metadata (the <i>general_term</i> rule in TPTP's grammar)
data GTerm
ColonSep :: GData -> GTerm -> GTerm
GTerm :: GData -> GTerm
GList :: [GTerm] -> GTerm
class FreeVars a
freeVars :: FreeVars a => a -> Set V

-- | Universally quantify all free variables in the formula
univquant_free_vars :: Formula -> Formula

-- | TPTP constant symbol/predicate symbol/function symbol identifiers
--   (they are output in single quotes unless they are <i>lower_word</i>s).
--   
--   Tip: Use the <tt>-XOverloadedStrings</tt> compiler flag if you don't
--   want to have to type <i>AtomicWord</i> to construct an
--   <a>AtomicWord</a>
newtype AtomicWord
AtomicWord :: String -> AtomicWord

-- | Variable names
newtype V
V :: String -> V

-- | This class is used in several utility functions involving <a>F</a> and
--   <a>T</a>.
--   
--   Conceptually <a>point</a> should be of type <tt>a -&gt; m a</tt>, but
--   we need the extra flexibility to make restricted monads like
--   <a>Set</a> instances.
--   
--   Note: We have <tt>instance (Monad m) =&gt; Pointed a (m a)</tt>, but
--   Haddock currently doesn't display this.
class Pointed a b | b -> a
point :: Pointed a b => a -> b

-- | This class is used in several utility functions involving <a>F</a> and
--   <a>T</a>.
--   
--   Conceptually <a>copoint</a> should be of type <tt>w a -&gt; a</tt>,
--   but let's keep the extra flexibility.
class Copointed a b | b -> a
copoint :: Copointed a b => b -> a
unwrapF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => F t -> Formula0 (T t) (F t)
unwrapT :: Copointed (Term0 (T t)) (t (Term0 (T t))) => T t -> Term0 (T t)
foldFormula0 :: (f -> r) -> (Quant -> [V] -> f -> r) -> (f -> BinOp -> f -> r) -> (t -> InfixPred -> t -> r) -> (AtomicWord -> [t] -> r) -> Formula0 t f -> r
foldTerm0 :: (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [t] -> r) -> Term0 t -> r

-- | Eliminate formulae
foldF :: Copointed (Formula0 (T t) (F t)) (t (Formula0 (T t) (F t))) => (F t -> r) -> (Quant -> [V] -> F t -> r) -> (F t -> BinOp -> F t -> r) -> (T t -> InfixPred -> T t -> r) -> (AtomicWord -> [T t] -> r) -> (F t -> r)

-- | Eliminate terms
foldT :: Copointed (Term0 (T t)) (t (Term0 (T t))) => (String -> r) -> (Rational -> r) -> (V -> r) -> (AtomicWord -> [T t] -> r) -> (T t -> r)
instance [overlap ok] Typeable BinOp
instance [overlap ok] Typeable InfixPred
instance [overlap ok] Typeable Quant
instance [overlap ok] Typeable Role
instance [overlap ok] Typeable AtomicWord
instance [overlap ok] Typeable V
instance [overlap ok] Typeable1 Term0
instance [overlap ok] Typeable2 Formula0
instance [overlap ok] Typeable GData
instance [overlap ok] Typeable GTerm
instance [overlap ok] Typeable UsefulInfo
instance [overlap ok] Typeable Annotations
instance [overlap ok] (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (F c)
instance [overlap ok] (Typeable1 c, Data (c (Term0 (T c)))) => Data (T c)
instance [overlap ok] Read (c (Formula0 (T c) (F c))) => Read (F c)
instance [overlap ok] Read (c (Term0 (T c))) => Read (T c)
instance [overlap ok] Show (c (Formula0 (T c) (F c))) => Show (F c)
instance [overlap ok] Show (c (Term0 (T c))) => Show (T c)
instance [overlap ok] Ord (c (Formula0 (T c) (F c))) => Ord (F c)
instance [overlap ok] Ord (c (Term0 (T c))) => Ord (T c)
instance [overlap ok] Eq (c (Formula0 (T c) (F c))) => Eq (F c)
instance [overlap ok] Eq (c (Term0 (T c))) => Eq (T c)
instance [overlap ok] (Typeable1 c, Data (c (Formula0 (T c) (F c)))) => Data (TPTP_Input_ c)
instance [overlap ok] Read (c (Formula0 (T c) (F c))) => Read (TPTP_Input_ c)
instance [overlap ok] Show (c (Formula0 (T c) (F c))) => Show (TPTP_Input_ c)
instance [overlap ok] Ord (c (Formula0 (T c) (F c))) => Ord (TPTP_Input_ c)
instance [overlap ok] Eq (c (Formula0 (T c) (F c))) => Eq (TPTP_Input_ c)
instance [overlap ok] Typeable1 Identity
instance [overlap ok] Data a => Data (Identity a)
instance [overlap ok] Read a => Read (Identity a)
instance [overlap ok] Show a => Show (Identity a)
instance [overlap ok] Ord a => Ord (Identity a)
instance [overlap ok] Eq a => Eq (Identity a)
instance [overlap ok] Eq BinOp
instance [overlap ok] Ord BinOp
instance [overlap ok] Show BinOp
instance [overlap ok] Read BinOp
instance [overlap ok] Data BinOp
instance [overlap ok] Enum BinOp
instance [overlap ok] Bounded BinOp
instance [overlap ok] Eq InfixPred
instance [overlap ok] Ord InfixPred
instance [overlap ok] Show InfixPred
instance [overlap ok] Read InfixPred
instance [overlap ok] Data InfixPred
instance [overlap ok] Enum InfixPred
instance [overlap ok] Bounded InfixPred
instance [overlap ok] Eq Quant
instance [overlap ok] Ord Quant
instance [overlap ok] Show Quant
instance [overlap ok] Read Quant
instance [overlap ok] Data Quant
instance [overlap ok] Enum Quant
instance [overlap ok] Bounded Quant
instance [overlap ok] Eq Role
instance [overlap ok] Ord Role
instance [overlap ok] Show Role
instance [overlap ok] Read Role
instance [overlap ok] Data Role
instance [overlap ok] Eq AtomicWord
instance [overlap ok] Ord AtomicWord
instance [overlap ok] Show AtomicWord
instance [overlap ok] Data AtomicWord
instance [overlap ok] Read AtomicWord
instance [overlap ok] Monoid AtomicWord
instance [overlap ok] IsString AtomicWord
instance [overlap ok] Eq V
instance [overlap ok] Ord V
instance [overlap ok] Show V
instance [overlap ok] Data V
instance [overlap ok] Read V
instance [overlap ok] Monoid V
instance [overlap ok] IsString V
instance [overlap ok] Eq term => Eq (Term0 term)
instance [overlap ok] Ord term => Ord (Term0 term)
instance [overlap ok] Show term => Show (Term0 term)
instance [overlap ok] Read term => Read (Term0 term)
instance [overlap ok] Data term => Data (Term0 term)
instance [overlap ok] (Eq term, Eq formula) => Eq (Formula0 term formula)
instance [overlap ok] (Ord term, Ord formula) => Ord (Formula0 term formula)
instance [overlap ok] (Show term, Show formula) => Show (Formula0 term formula)
instance [overlap ok] (Read term, Read formula) => Read (Formula0 term formula)
instance [overlap ok] (Data term, Data formula) => Data (Formula0 term formula)
instance [overlap ok] Eq GData
instance [overlap ok] Ord GData
instance [overlap ok] Show GData
instance [overlap ok] Read GData
instance [overlap ok] Data GData
instance [overlap ok] Eq GTerm
instance [overlap ok] Ord GTerm
instance [overlap ok] Show GTerm
instance [overlap ok] Read GTerm
instance [overlap ok] Data GTerm
instance [overlap ok] Eq UsefulInfo
instance [overlap ok] Ord UsefulInfo
instance [overlap ok] Show UsefulInfo
instance [overlap ok] Read UsefulInfo
instance [overlap ok] Data UsefulInfo
instance [overlap ok] Eq Annotations
instance [overlap ok] Ord Annotations
instance [overlap ok] Show Annotations
instance [overlap ok] Read Annotations
instance [overlap ok] Data Annotations
instance [overlap ok] Copointed a (Identity a)
instance [overlap ok] Monad m => Pointed a (m a)
instance [overlap ok] Typeable1 c => Typeable (T c)
instance [overlap ok] Typeable1 c => Typeable (F c)
instance [overlap ok] Arbitrary V
instance [overlap ok] Arbitrary AtomicWord
instance [overlap ok] Arbitrary GTerm
instance [overlap ok] Arbitrary GData
instance [overlap ok] Arbitrary a => Arbitrary (Term0 a)
instance [overlap ok] Arbitrary Quant
instance [overlap ok] Arbitrary InfixPred
instance [overlap ok] Arbitrary BinOp
instance [overlap ok] (Arbitrary a, Arbitrary b) => Arbitrary (Formula0 a b)
instance [overlap ok] Arbitrary Role
instance [overlap ok] Arbitrary UsefulInfo
instance [overlap ok] Arbitrary Annotations
instance [overlap ok] Arbitrary Term
instance [overlap ok] Arbitrary Formula
instance [overlap ok] Arbitrary TPTP_Input
instance [overlap ok] FreeVars Term
instance [overlap ok] FreeVars Formula
instance [overlap ok] Typeable1 c => Typeable (TPTP_Input_ c)

module Codec.TPTP.Export

-- | Convenient wrapper for <a>toTPTP</a>
toTPTP' :: ToTPTP a => a -> String
class ToTPTP a
toTPTP :: ToTPTP a => a -> ShowS
isLowerWord :: [Char] -> Bool
instance [overlap ok] ToTPTP (T Identity)
instance [overlap ok] ToTPTP (F Identity)
instance [overlap ok] ToTPTP a => ToTPTP (Identity a)
instance [overlap ok] ToTPTP V
instance [overlap ok] ToTPTP GData
instance [overlap ok] ToTPTP AtomicWord
instance [overlap ok] ToTPTP GTerm
instance [overlap ok] ToTPTP UsefulInfo
instance [overlap ok] ToTPTP Annotations
instance [overlap ok] ToTPTP t => ToTPTP (Term0 t)
instance [overlap ok] (ToTPTP f, ToTPTP t) => ToTPTP (Formula0 t f)
instance [overlap ok] ToTPTP BinOp
instance [overlap ok] ToTPTP InfixPred
instance [overlap ok] ToTPTP Quant
instance [overlap ok] ToTPTP Role
instance [overlap ok] ToTPTP TPTP_Input
instance [overlap ok] ToTPTP [TPTP_Input]


-- | Mainly just <a>Pretty</a> instances
module Codec.TPTP.Pretty
prettySimple :: Pretty a => a -> String

-- | Carries information about the enclosing operation (for the purpose of
--   printing stuff without parentheses if possible).
data WithEnclosing a
WithEnclosing :: Enclosing -> a -> WithEnclosing a
data Enclosing
EnclBinOp :: BinOp -> Enclosing
EnclQuant :: Enclosing
EnclNeg :: Enclosing
EnclInfixPred :: InfixPred -> Enclosing
EnclNothing :: Enclosing
instance [overlap ok] Typeable Enclosing
instance [overlap ok] Pretty a => Pretty (Identity a)
instance [overlap ok] Pretty (T Identity)
instance [overlap ok] Pretty (F Identity)
instance [overlap ok] Eq Enclosing
instance [overlap ok] Ord Enclosing
instance [overlap ok] Show Enclosing
instance [overlap ok] Data Enclosing
instance [overlap ok] Read Enclosing
instance [overlap ok] Pretty V
instance [overlap ok] Pretty GTerm
instance [overlap ok] Pretty AtomicWord
instance [overlap ok] Pretty GData
instance [overlap ok] Pretty UsefulInfo
instance [overlap ok] Pretty Annotations
instance [overlap ok] Pretty (WithEnclosing Term)
instance [overlap ok] Pretty (WithEnclosing Formula)
instance [overlap ok] Pretty (Term0 Term)
instance [overlap ok] Pretty (Formula0 Term Formula)
instance [overlap ok] Pretty (WithEnclosing t) => Pretty (WithEnclosing (Term0 t))
instance [overlap ok] Pretty InfixPred
instance [overlap ok] Pretty BinOp
instance [overlap ok] (Pretty (WithEnclosing t), Pretty (WithEnclosing f)) => Pretty (WithEnclosing (Formula0 t f))
instance [overlap ok] Pretty Quant
instance [overlap ok] Pretty TPTP_Input

module Codec.TPTP.Diff
class Diffable a b
diff :: Diffable a b => a -> a -> b
data DiffResult d

-- | Both arguments are the same.
Same :: DiffResult d

-- | The arguments are recursive expressions of the same form, but their
--   subterms differ. Return a "decorated" term that shows where the
--   differences are
SameHead :: d -> DiffResult d

-- | The arguments differ and are not of similar form (don't recurse)
Differ :: d -> d -> DiffResult d
DontCare :: DiffResult d
type T0Diff = DiffResult (Term0 (T DiffResult))
type F0Diff = DiffResult (Formula0 (T DiffResult) (F DiffResult))
isSame :: DiffResult t -> Bool

-- | Less random generator for generating formulae suitable for testing
--   diff
diffGenF :: Gen Formula
diffGenT :: Gen Term
printSampleDiffs :: IO ()
instance [overlap ok] Typeable1 DiffResult
instance [overlap ok] Pretty (F DiffResult)
instance [overlap ok] Pretty (T DiffResult)
instance [overlap ok] Eq d => Eq (DiffResult d)
instance [overlap ok] Ord d => Ord (DiffResult d)
instance [overlap ok] Show d => Show (DiffResult d)
instance [overlap ok] Data d => Data (DiffResult d)
instance [overlap ok] Read d => Read (DiffResult d)
instance [overlap ok] Diffable Term (T DiffResult)
instance [overlap ok] Diffable Formula (F DiffResult)
instance [overlap ok] Functor DiffResult
instance [overlap ok] Pretty F0Diff
instance [overlap ok] Pretty T0Diff
instance [overlap ok] Pretty (WithEnclosing (F DiffResult))
instance [overlap ok] Pretty (WithEnclosing (T DiffResult))
instance [overlap ok] Pretty (WithEnclosing F0Diff)
instance [overlap ok] Pretty (WithEnclosing T0Diff)
instance [overlap ok] Show (F DiffResult)
instance [overlap ok] Show (T DiffResult)

module Codec.TPTP.Import
parse :: String -> [TPTP_Input]
parseFile :: FilePath -> IO [TPTP_Input]
parseWithComment :: String -> [TPTP_Input_C]
parseWithCommentFile :: FilePath -> IO [TPTP_Input_C]
data Token
LP :: Token
RP :: Token
Comma :: Token
Dot :: Token
Lbrack :: Token
Rbrack :: Token
Oper :: String -> Token
SingleQuoted :: String -> Token
DoubleQuoted :: String -> Token
DollarWord :: String -> Token
DollarDollarWord :: String -> Token
UpperWord :: String -> Token
LowerWord :: String -> Token
Star :: Token
Plus :: Token
Rangle :: Token
SignedInt :: Integer -> Token
UnsignedInt :: Integer -> Token
Real :: Rational -> Token
CommentToken :: String -> Token
Slash :: Token

module Codec.TPTP